1  /-
  2  Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Zhouhang Zhou
  5  -/
  6  
  7  import measure_theory.ae_eq_fun
src         └──────────────────────┘
  8  
  9  /-!
 10  # Integrable functions and `L¹` space
 11  
 12  In the first part of this file, the predicate `integrable` is defined and basic properties of
 13  integrable functions are proved.
 14  
 15  In the second part, the space `L¹` of equivalence classes of integrable functions under the relation
 16  of being almost everywhere equal is defined as a subspace of the space `L⁰`. See the file
 17  `src/measure_theory/ae_eq_fun.lean` for information on `L⁰` space.
 18  
 19  ## Notation
 20  
 21  * `α →₁ β` is the type of `L¹` space, where `α` is a `measure_space` and `β` is a `normed_group` with
 22    a `second_countable_topology`. `f : α →ₘ β` is a "function" in `L¹`. In comments, `[f]` is also used
 23    to denote an `L¹` function.
 24  
 25    `₁` can be typed as `\1`.
 26  
 27  ## Main definitions
 28  
 29  * Let `f : α → β` be a function, where `α` is a `measure_space` and `β` a `normed_group`.
 30    Then `f` is called `integrable` if `(∫⁻ a, nnnorm (f a)) < ⊤` holds.
 31  
 32  * The space `L¹` is defined as a subspace of `L⁰` :
 33    An `ae_eq_fun` `[f] : α →ₘ β` is in the space `L¹` if `edist [f] 0 < ⊤`, which means
 34    `(∫⁻ a, edist (f a) 0) < ⊤` if we expand the definition of `edist` in `L⁰`.
 35  
 36  ## Main statements
 37  
 38  `L¹`, as a subspace, inherits most of the structures of `L⁰`.
 39  
 40  ## Implementation notes
 41  
 42  Maybe `integrable f` should be mean `(∫⁻ a, edist (f a) 0) < ⊤`, so that `integrable` and
 43  `ae_eq_fun.integrable` are more aligned. But in the end one can use the lemma
 44  `lintegral_nnnorm_eq_lintegral_edist : (∫⁻ a, nnnorm (f a)) = (∫⁻ a, edist (f a) 0)` to switch the
 45  two forms.
 46  
 47  ## Tags
 48  
 49  integrable, function space, l1
 50  
 51  -/
 52  
 53  noncomputable theory
 54  open_locale classical topological_space
 55  
 56  set_option class.instance_max_depth 100
doc             └──────────────────────┘
 57  
 58  namespace measure_theory
 59  open set lattice filter topological_space ennreal emetric
 60  
 61  universes u v w
 62  variables {α : Type u} [measure_space α]
id                          └───────────┘
src                          └───────────┘
typ                         └───────────┘
doc                          └───────────┘
 63  variables {β : Type v} [normed_group β] {γ : Type w} [normed_group γ]
id                           └──────────┘                  └──────────┘
src                          └──────────┘                  └──────────┘
typ                          └──────────┘                  └──────────┘
doc                          └──────────┘                  └──────────┘
 64  
 65  /-- A function is `integrable` if the integral of its pointwise norm is less than infinity. -/
 66  def integrable (f : α → β) : Prop := (∫⁻ a, nnnorm (f a)) < ⊤
id                                       └┘  └────┘       
src                                        └┘   └────┘         
typ                                      └┘  └────┘       
doc                                        └┘   └────┘
 67  
 68  lemma integrable_iff_norm (f : α → β) : integrable f ↔ (∫⁻ a, ennreal.of_real ∥f a∥) < ⊤ :=
id                                         └────────┘    └┘  └─────────────┘     
src                                          └────────┘     └┘   └─────────────┘       
typ                                        └────────┘    └┘  └─────────────┘     
doc                                          └────────┘      └┘   └─────────────┘
 69  have eq : (λa, ennreal.of_real ∥f a∥) = (λa, (nnnorm(f a) : ennreal)),
id                 └─────────────┘          └────┘      └─────┘
src                 └─────────────┘             └────┘        └─────┘
typ                └─────────────┘          └────┘      └─────┘
doc                 └─────────────┘                └────┘        └─────┘
 70    by { funext, rw of_real_norm_eq_coe_nnnorm },
id                     └────────────────────────┘
src         └────┘  └─┘└────────────────────────┘
typ         └────┘  └─┘└────────────────────────┘
doc         └────┘  └─┘                          
txt         └────┘  └─┘                          
par         └────┘  └─┘                          
pid                                             
st       └───────┘└──────────────────────────────┘└┘
 71  iff.intro (by { rw eq, exact λh, h }) $ by { rw eq, exact λh, h }
id   └───────┘          └┘                           └┘
src  └───────┘       └─┘└┘  └────┘ └─┘           └─┘└┘  └────┘ └─┘ 
typ  └───────┘       └─┘└┘  └────┘ └─┘           └─┘└┘  └────┘ └─┘ 
doc                  └─┘    └────┘ └─┘           └─┘    └────┘ └─┘ 
txt                  └─┘    └────┘ └─┘           └─┘    └────┘ └─┘ 
par                  └─┘    └────┘ └─┘           └─┘    └────┘ └─┘ 
pid                              └─┘                       └─┘ 
st                └──────┘└────────────┘└┘     └──────┘└────────────┘└┘
 72  
 73  lemma integrable_iff_edist (f : α → β) : integrable f ↔ (∫⁻ a, edist (f a) 0) < ⊤ :=
id                                          └────────┘    └┘  └───┘         
src                                           └────────┘     └┘   └───┘           
typ                                         └────────┘    └┘  └───┘         
doc                                           └────────┘      └┘  
 74  have eq : (λa, edist (f a) 0) = (λa, (nnnorm(f a) : ennreal)),
id                 └───┘              └────┘      └─────┘
src                 └───┘                 └────┘        └─────┘
typ                └───┘              └────┘      └─────┘
doc                                        └────┘        └─────┘
 75    by { funext, rw edist_eq_coe_nnnorm },
id                     └─────────────────┘
src         └────┘  └─┘└─────────────────┘
typ         └────┘  └─┘└─────────────────┘
doc         └────┘  └─┘                   
txt         └────┘  └─┘                   
par         └────┘  └─┘                   
pid                                      
st       └───────┘└───────────────────────┘└┘
 76  iff.intro (by { rw eq, exact λh, h }) $ by { rw eq, exact λh, h }
id   └───────┘          └┘                           └┘
src  └───────┘       └─┘└┘  └────┘ └─┘           └─┘└┘  └────┘ └─┘ 
typ  └───────┘       └─┘└┘  └────┘ └─┘           └─┘└┘  └────┘ └─┘ 
doc                  └─┘    └────┘ └─┘           └─┘    └────┘ └─┘ 
txt                  └─┘    └────┘ └─┘           └─┘    └────┘ └─┘ 
par                  └─┘    └────┘ └─┘           └─┘    └────┘ └─┘ 
pid                              └─┘                       └─┘ 
st                └──────┘└────────────┘└┘     └──────┘└────────────┘└┘
 77  
 78  lemma integrable_iff_of_real {f : α → ℝ} (h : ∀ₘ a, 0 ≤ f a) :
id                                               └┘      
src                                               └┘     
typ                                              └┘      
doc                                                └┘  
 79    integrable f ↔ (∫⁻ a, ennreal.of_real (f a)) < ⊤ :=
id     └────────┘    └┘  └─────────────┘       
src    └────────┘     └┘   └─────────────┘         
typ    └────────┘    └┘  └─────────────┘       
doc    └────────┘      └┘   └─────────────┘
 80  have lintegral_eq :  (∫⁻ a, ennreal.of_real ∥f a∥) = (∫⁻ a, ennreal.of_real (f a)) :=
id                         └┘  └─────────────┘      └┘  └─────────────┘   
src                        └┘   └─────────────┘        └┘   └─────────────┘
typ                        └┘  └─────────────┘      └┘  └─────────────┘   
doc                        └┘   └─────────────┘           └┘   └─────────────┘
 81  begin
st   └─────
 82    apply lintegral_congr_ae,
id           └────────────────┘
src    └────┘└────────────────┘
typ    └────┘└────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────┘└─
 83    filter_upwards [h],
src    └──────────────┘ 
typ    └──────────────┘ 
doc    └──────────────┘ 
txt    └──────────────┘ 
par    └──────────────┘ 
pid                  └┘ 
st   ───────────────────┘└─
 84    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
 85    assume a h,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid    └────────┘
st   ───────────┘└─
 86    rw [real.norm_eq_abs, abs_of_nonneg],
id         └──────────────┘  └───────────┘
src    └──┘└──────────────┘└┘└───────────┘
typ    └──┘└──────────────┘└┘└───────────┘
doc    └──┘                └┘             
txt    └──┘                └┘             
par    └──┘                └┘             
pid      └┘                └┘             
st   ─────────────────────┘└─────────────┘└──
 87    exact h
id           
src    └────┘ 
typ    └────┘
doc    └────┘ 
txt    └────┘ 
par    └────┘ 
pid          
st   ─────────┘
 88  end,
st   └─┘
 89  by rw [integrable_iff_norm, lintegral_eq]
id          └─────────────────┘  └──────────┘
src     └──┘└─────────────────┘└┘            └─
typ     └──┘└─────────────────┘└┘└──────────┘└─
doc     └──┘                   └┘            └─
txt     └──┘                   └┘            └─
par     └──┘                   └┘            └─
pid       └┘                   └┘            
st     └──────────────────────┘└────────────┘
 90  
src  
typ  
doc  
txt  
par  
pid  
st   
 91  lemma integrable_of_ae_eq {f g : α → β} (hf : integrable f) (h : ∀ₘ a, f a = g a) : integrable g :=
id                                               └────────┘        └┘          └────────┘ 
src                                                └────────┘         └┘               └────────┘
typ                                              └────────┘        └┘          └────────┘ 
doc                                                └────────┘         └┘                └────────┘
 92  begin
st   └─────
 93    simp only [integrable] at *,
id                └────────┘
src    └─────────┘└────────┘└────┘
typ    └─────────┘└────────┘└────┘
doc    └─────────┘└────────┘└────┘
txt    └─────────┘          └────┘
par    └─────────┘          └────┘
pid        └──┘└┘          └──┘
st   ────────────────────────────┘└─
 94    have : (∫⁻ (a : α), ↑(nnnorm (f a))) = (∫⁻ (a : α), ↑(nnnorm (g a))),
id                                          └┘          └────┘  
src    └─────┘   └────┘            └──┘ └┘└────┘   └────┘   └─┘
typ    └─────┘   └────┘           └──┘ └┘└────┘  └────┘  └─┘
doc    └─────┘   └────┘             └──┘  └┘└────┘   └────┘   └─┘
txt    └─────┘   └────┘             └──┘    └────┘             └─┘
par    └─────┘   └────┘             └──┘    └────┘             └─┘
pid    └───┘└┘   └────┘             └──┘    └────┘             └─┘
st   ─────────────────────────────────────────────────────────────────────┘└─
 95    { apply lintegral_congr_ae,
id             └────────────────┘
src      └────┘└────────────────┘
typ      └────┘└────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└──────────────────────┘└─
 96      filter_upwards [h],
src      └──────────────┘ 
typ      └──────────────┘ 
doc      └──────────────┘ 
txt      └──────────────┘ 
par      └──────────────┘ 
pid                    └┘ 
st   ─────────────────────┘└─
 97      assume a,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
 98      simp only [mem_set_of_eq],
id                  └───────────┘
src      └─────────┘└───────────┘
typ      └─────────┘└───────────┘
doc      └─────────┘             
txt      └─────────┘             
par      └─────────┘             
pid          └──┘└┘             
st   ────────────────────────────┘└─
 99      assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
100      rw h },
id          
src      └─┘ 
typ      └─┘
doc      └─┘ 
txt      └─┘ 
par      └─┘ 
pid         
st   ────────┘└┘
101    rwa ← this
id           └──┘
src    └────┘    
typ    └────┘└──┘
doc    └────┘    
txt    └────┘    
par    └────┘    
pid       └─┘    
st   ────────────┘
102  end
st   └─┘
103  
104  lemma integrable_congr_ae {f g : α → β} (h : ∀ₘ a, f a = g a) : integrable f ↔ integrable g :=
id                                              └┘          └────────┘   └────────┘ 
src                                               └┘               └────────┘    └────────┘
typ                                             └┘          └────────┘   └────────┘ 
doc                                               └┘                └────────┘     └────────┘
st                                  
105  iff.intro (λhf, integrable_of_ae_eq hf h) (λhg, integrable_of_ae_eq hg (all_ae_eq_symm h))
id   └───────┘   └┘  └─────────────────┘ └┘     └┘  └─────────────────┘ └┘  └────────────┘ 
src  └───────┘       └─────────────────┘             └─────────────────┘     └────────────┘
typ  └───────┘   └┘  └─────────────────┘ └┘     └┘  └─────────────────┘ └┘  └────────────┘ 
st                  
106  
107  lemma integrable_of_le_ae {f : α → β} {g : α → γ} (h : ∀ₘ a, ∥f a∥ ≤ ∥g a∥) (hg : integrable g) :
id                                                      └┘              └────────┘ 
src                                                         └┘                   └────────┘
typ                                                     └┘              └────────┘ 
doc                                                         └┘                        └────────┘
108    integrable f :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
109  begin
st   └─────
110    simp only [integrable_iff_norm] at *,
id                └─────────────────┘
src    └─────────┘└─────────────────┘└────┘
typ    └─────────┘└─────────────────┘└────┘
doc    └─────────┘                   └────┘
txt    └─────────┘                   └────┘
par    └─────────┘                   └────┘
pid        └──┘└┘                   └──┘
st   ─────────────────────────────────────┘└─
111    calc (∫⁻ a, ennreal.of_real ∥f a∥) ≤ (∫⁻ (a : α), ennreal.of_real ∥g a∥) :
id     └──┘  └┘                                    └─────────────┘  
src    └──┘  └┘                                       └─────────────┘
typ    └──┘  └┘                                    └─────────────┘  
doc    └──┘  └┘                                         └─────────────┘
st   ─────────────────────────────────────────────────────────────────────────────
112      lintegral_le_lintegral_ae (by { filter_upwards [h], assume a h, exact of_real_le_of_real h })
id       └───────────────────────┘                                             └────────────────┘ 
src      └───────────────────────┘       └──────────────┘   └────────┘  └────┘└────────────────┘ 
typ      └───────────────────────┘       └──────────────┘   └────────┘  └────┘└────────────────┘
doc                                      └──────────────┘   └────────┘  └────┘                   
txt                                      └──────────────┘   └────────┘  └────┘                   
par                                      └──────────────┘   └────────┘  └────┘                   
pid                                                    └┘   └────────┘                          
st   ────────────────────────────────┘└───────────────────┘└──────────┘└───────────────────────────┘└┘
113      ... < ⊤ : hg
id                └┘
src            
typ               └┘
st   ───────────────┘
114  end
st   ──┘
115  
116  lemma integrable_of_le {f : α → β} {g : α → γ} (h : ∀a, ∥f a∥ ≤ ∥g a∥) (hg : integrable g) :
id                                                                  └────────┘ 
src                                                                          └────────┘
typ                                                                 └────────┘ 
doc                                                                               └────────┘
117    integrable f :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
118  integrable_of_le_ae (univ_mem_sets' h) hg
id   └─────────────────┘  └────────────┘   └┘
src  └─────────────────┘  └────────────┘
typ  └─────────────────┘  └────────────┘   └┘
119  
120  lemma lintegral_nnnorm_eq_lintegral_edist (f : α → β) :
id                                                     
typ                                                    
121    (∫⁻ a, nnnorm (f a)) = ∫⁻ a, edist (f a) 0 :=
id      └┘  └────┘       └┘  └───┘   
src     └┘   └────┘         └┘   └───┘
typ     └┘  └────┘       └┘  └───┘   
doc     └┘   └────┘          └┘  
122  by { congr, funext, rw edist_eq_coe_nnnorm }
id                          └─────────────────┘
src       └───┘  └────┘  └─┘└─────────────────┘
typ       └───┘  └────┘  └─┘└─────────────────┘
doc              └────┘  └─┘                   
txt       └───┘  └────┘  └─┘                   
par       └───┘  └────┘  └─┘                   
pid                                           
st     └──────┘└──────┘└───────────────────────┘└┘
123  
124  lemma lintegral_norm_eq_lintegral_edist (f : α → β) :
id                                                   
typ                                                  
125    (∫⁻ a, ennreal.of_real ∥f a∥) = ∫⁻ a, edist (f a) 0 :=
id      └┘  └─────────────┘     └┘  └───┘   
src     └┘   └─────────────┘       └┘   └───┘
typ     └┘  └─────────────┘     └┘  └───┘   
doc     └┘   └─────────────┘          └┘  
126  by { congr, funext, rw [of_real_norm_eq_coe_nnnorm, edist_eq_coe_nnnorm] }
id                           └────────────────────────┘  └─────────────────┘
src       └───┘  └────┘  └──┘└────────────────────────┘└┘└─────────────────┘└┘
typ       └───┘  └────┘  └──┘└────────────────────────┘└┘└─────────────────┘└┘
doc              └────┘  └──┘                          └┘                   └┘
txt       └───┘  └────┘  └──┘                          └┘                   └┘
par       └───┘  └────┘  └──┘                          └┘                   └┘
pid                        └┘                          └┘                   
st     └──────┘└──────┘└──────────────────────────────┘└───────────────────┘└┘
127  
128  lemma lintegral_edist_triangle [second_countable_topology β] {f g h : α → β}
id                                   └───────────────────────┘               
src                                  └───────────────────────┘
typ                                  └───────────────────────┘               
doc                                  └───────────────────────┘
129    (hf : measurable f) (hg : measurable g) (hh : measurable h) :
id           └────────┘         └────────┘         └────────┘ 
src          └────────┘          └────────┘          └────────┘
typ          └────────┘         └────────┘         └────────┘ 
doc          └────────┘          └────────┘          └────────┘
130    (∫⁻ a, edist (f a) (g a)) ≤ (∫⁻ a, edist (f a) (h a)) + ∫⁻ a, edist (g a) (h a) :=
id      └┘  └───┘            └┘  └───┘           └┘  └───┘       
src     └┘   └───┘                └┘   └───┘               └┘   └───┘
typ     └┘  └───┘            └┘  └───┘           └┘  └───┘       
doc     └┘                         └┘                        └┘  
131  begin
st   └─────
132    rw ← lintegral_add (measurable.edist hf hh) (measurable.edist hg hh),
id          └───────────┘                   └┘      └──────────────┘ └┘ └┘
src    └───┘└───────────┘                     └┘ └──────────────┘    
typ    └───┘└───────────┘                 └┘  └┘ └──────────────┘└┘└┘
doc    └───┘                                  └┘                     
txt    └───┘                                  └┘                     
par    └───┘                                  └┘                     
pid      └─┘                                  └┘                     
st   ─────────────────────────────────────────────────────────────────────┘└─
133    apply lintegral_le_lintegral,
id           └────────────────────┘
src    └────┘└────────────────────┘
typ    └────┘└────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────────┘└─
134    assume a,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
135    have := edist_triangle (f a) (h a) (g a),
id             └────────────┘             
src    └──────┘└────────────┘   └┘   └┘   
typ    └──────┘└────────────┘  └┘  └┘ 
doc    └──────┘                 └┘   └┘   
txt    └──────┘                 └┘   └┘   
par    └──────┘                 └┘   └┘   
pid    └───┘└─┘                 └┘   └┘   
st   ─────────────────────────────────────────┘└─
136    convert this,
id             └──┘
src    └──────┘
typ    └──────┘└──┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid           
st   ─────────────┘└─
137    rw edist_comm (h a) (g a),
id        └────────┘        
src    └─┘└────────┘   └┘   
typ    └─┘└────────┘  └┘ 
doc    └─┘             └┘   
txt    └─┘             └┘   
par    └─┘             └┘   
pid                   └┘   
st   ──────────────────────────┘└─
138  end
st   ──┘
139  
140  lemma lintegral_edist_lt_top [second_countable_topology β] {f g : α → β}
id                                 └───────────────────────┘             
src                                └───────────────────────┘
typ                                └───────────────────────┘             
doc                                └───────────────────────┘
141    (hfm : measurable f) (hfi : integrable f) (hgm : measurable g) (hgi : integrable g) :
id            └────────┘          └────────┘          └────────┘          └────────┘ 
src           └────────┘           └────────┘           └────────┘           └────────┘
typ           └────────┘          └────────┘          └────────┘          └────────┘ 
doc           └────────┘           └────────┘           └────────┘           └────────┘
142    (∫⁻ a, edist (f a) (g a)) < ⊤ :=
id      └┘  └───┘           
src     └┘   └───┘               
typ     └┘  └───┘           
doc     └┘  
143  lt_of_le_of_lt
id   └────────────┘
src  └────────────┘
typ  └────────────┘
144    (lintegral_edist_triangle hfm hgm (measurable_const : measurable (λa, (0 : β))))
id      └──────────────────────┘ └─┘ └─┘  └──────────────┘   └────────┘          
src     └──────────────────────┘          └──────────────┘   └────────┘
typ     └──────────────────────┘ └─┘ └─┘  └──────────────┘   └────────┘          
doc                                                          └────────┘
145    (ennreal.add_lt_top.2 $ by { split; rw ← integrable_iff_edist; assumption })
id      └────────────────┘                     └──────────────────┘
src     └────────────────┘         └───┘  └───┘└──────────────────┘  └─────────┘
typ     └────────────────┘         └───┘  └───┘└──────────────────┘  └─────────┘
doc                                 └───┘  └───┘                      └─────────┘
txt                                 └───┘  └───┘                      └─────────┘
par                                 └───┘  └───┘                      └─────────┘
pid                                          └─┘                                
st                               └──────────────────────────────────────────────┘└┘
146  
147  @[simp] lemma lintegral_nnnorm_zero : (∫⁻ a : α, nnnorm (0 : β)) = 0 := by simp
id                                          └┘      └────┘         
src                                         └┘       └────┘                   └────
typ                                         └┘      └────┘                  └────
doc    └──┘                                 └┘       └────┘                    └────
txt                                                                             └────
par                                                                             └────
pid                                                                                 
st                                                                             └─────
148  
src  
typ  
doc  
txt  
par  
pid  
st   
149  variables (α β)
150  @[simp] lemma integrable_zero : integrable (λa:α, (0:β)) :=
id                                   └────────┘          
src                                  └────────┘
typ                                  └────────┘          
doc    └──┘                          └────────┘
151  by { have := coe_lt_top, simpa [integrable] }
id                └────────┘         └────────┘
src       └──────┘└────────┘  └─────┘└────────┘└┘
typ       └──────┘└────────┘  └─────┘└────────┘└┘
doc       └──────┘            └─────┘└────────┘└┘
txt       └──────┘            └─────┘          └┘
par       └──────┘            └─────┘          └┘
pid       └───┘└─┘                           
st     └───────────────────┘└───────────────────┘└┘
152  variables {α β}
153  
154  lemma lintegral_nnnorm_add {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) :
id                                                        └────────┘         └────────┘ 
src                                                           └────────┘          └────────┘
typ                                                       └────────┘         └────────┘ 
doc                                                           └────────┘          └────────┘
155    (∫⁻ a, nnnorm (f a) + nnnorm (g a)) = (∫⁻ a, nnnorm (f a)) + ∫⁻ a, nnnorm (g a) :=
id      └┘  └────┘      └────┘        └┘  └────┘       └┘  └────┘   
src     └┘   └────┘        └────┘          └┘   └────┘         └┘   └────┘
typ     └┘  └────┘      └────┘        └┘  └────┘       └┘  └────┘   
doc     └┘   └────┘         └────┘           └┘   └────┘          └┘   └────┘
156  lintegral_add (measurable.coe_nnnorm hf) (measurable.coe_nnnorm hg)
id   └───────────┘  └───────────────────┘ └┘   └───────────────────┘ └┘
src  └───────────┘  └───────────────────┘      └───────────────────┘
typ  └───────────┘  └───────────────────┘ └┘   └───────────────────┘ └┘
157  
158  lemma integrable.add {f g : α → β} (hfm : measurable f) (hfi : integrable f) (hgm : measurable g)
id                                           └────────┘          └────────┘          └────────┘ 
src                                            └────────┘           └────────┘           └────────┘
typ                                          └────────┘          └────────┘          └────────┘ 
doc                                            └────────┘           └────────┘           └────────┘
159    (hgi : integrable g): integrable (λa, f a + g a) :=
id            └────────┘    └────────┘         
src           └────────┘     └────────┘          
typ           └────────┘    └────────┘         
doc           └────────┘     └────────┘
160  calc
161    (∫⁻ (a : α), ↑(nnnorm ((f + g) a))) ≤ ∫⁻ (a : α), ↑(nnnorm (f a)) + ↑(nnnorm (g a)) :
id      └┘         └────┘             └┘         └────┘        └────┘   
src     └┘          └────┘                └┘          └────┘          └────┘
typ     └┘         └────┘             └┘         └────┘        └────┘   
doc     └┘           └────┘                 └┘           └────┘            └────┘
162      lintegral_le_lintegral _ _
id       └────────────────────┘
src      └────────────────────┘
typ      └────────────────────┘
163        (assume a, by { simp only [coe_add.symm, coe_le_coe], exact nnnorm_add_le _ _ })
id                                                 └────────┘         └───────────┘
src                        └─────────┘            └┘└────────┘  └────┘└───────────┘└───┘
typ                       └─────────┘└──────────┘└┘└────────┘  └────┘└───────────┘└───┘
doc                        └─────────┘            └┘            └────┘             └───┘
txt                        └─────────┘            └┘            └────┘             └───┘
par                        └─────────┘            └┘            └────┘             └───┘
pid                            └──┘└┘            └┘                              └──┘
st                      └─────────────────────────────────────┘└────────────────────────┘└┘
164    ... = _ :
165      lintegral_nnnorm_add hfm hgm
id       └──────────────────┘ └─┘ └─┘
src      └──────────────────┘
typ      └──────────────────┘ └─┘ └─┘
166    ... < ⊤ : add_lt_top.2 ⟨hfi, hgi⟩
id              └────────┘   └─┘  └─┘
src             └────────┘
typ             └────────┘   └─┘  └─┘
167  
168  lemma integrable_finset_sum {ι} [second_countable_topology β] (s : finset ι) {f : ι → α → β}
id                                    └───────────────────────┘        └────┘              
src                                   └───────────────────────┘         └────┘
typ                                   └───────────────────────┘        └────┘              
doc                                   └───────────────────────┘         └────┘
169    (hfm : ∀ i, measurable (f i)) (hfi : ∀ i, integrable (f i)) :
id                └────────┘                 └────────┘   
src                └────────┘                    └────────┘
typ               └────────┘                 └────────┘   
doc                └────────┘                    └────────┘
170    integrable (λ a, s.sum (λ i, f i a)) :=
id     └────────┘      └──┘        
src    └────────┘        └──┘
typ    └────────┘      └──┘        
doc    └────────┘
171  begin
st   └─────
172    refine finset.induction_on s _ _,
id            └─────────────────┘ 
src    └─────┘└─────────────────┘ └──┘
typ    └─────┘└─────────────────┘└──┘
doc    └─────┘└─────────────────┘ └──┘
txt    └─────┘                    └──┘
par    └─────┘                    └──┘
pid                              └──┘
st   ─────────────────────────────────┘└─
173    { simp only [finset.sum_empty, integrable_zero] },
id                  └──────────────┘  └─────────────┘
src      └─────────┘└──────────────┘└┘└─────────────┘└┘
typ      └─────────┘└──────────────┘└┘└─────────────┘└┘
doc      └─────────┘                └┘               └┘
txt      └─────────┘                └┘               └┘
par      └─────────┘                └┘               └┘
pid          └──┘└┘                └┘               
st   ───┘└────────────────────────────────────────────┘└┘
174    { assume i s his ih,
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
txt      └───────────────┘
par      └───────────────┘
pid      └───────────────┘
st   ────────────────────┘└─
175      simp only [his, finset.sum_insert, not_false_iff],
id                  └─┘  └───────────────┘  └───────────┘
src      └─────────┘   └┘└───────────────┘└┘└───────────┘
typ      └─────────┘└─┘└┘└───────────────┘└┘└───────────┘
doc      └─────────┘   └┘                 └┘             
txt      └─────────┘   └┘                 └┘             
par      └─────────┘   └┘                 └┘             
pid          └──┘└┘   └┘                 └┘             
st   ────────────────────────────────────────────────────┘└─
176      refine (hfi _).add (hfm _) (measurable_finset_sum s hfm) ih }
id               └─┘                 └───────────────────┘  └─┘  └┘
src      └─────┘    └──────┘    └──┘ └───────────────────┘    └┘  
typ      └─────┘ └─┘└──────┘    └──┘ └───────────────────┘└─┘└┘└┘
doc      └─────┘    └──────┘    └──┘                          └┘  
txt      └─────┘    └──────┘    └──┘                          └┘  
par      └─────┘    └──────┘    └──┘                          └┘  
pid                └──────┘    └──┘                          └┘  
st   ───────────────────────────────────────────────────────────────┘└─
177  end
st   ──┘
178  
179  lemma lintegral_nnnorm_neg {f : α → β} :
id                                      
typ                                     
180    (∫⁻ (a : α), ↑(nnnorm ((-f) a))) = ∫⁻ (a : α), ↑(nnnorm ((f) a)) :=
id      └┘         └────┘          └┘         └────┘     
src     └┘          └────┘            └┘          └────┘
typ     └┘         └────┘          └┘         └────┘     
doc     └┘           └────┘              └┘           └────┘
181  lintegral_congr_ae $ by { filter_upwards [], simp }
id   └────────────────┘
src  └────────────────┘        └───────────────┘  └───┘
typ  └────────────────┘        └───────────────┘  └───┘
doc                            └───────────────┘  └───┘
txt                            └───────────────┘  └───┘
par                            └───────────────┘  └───┘
pid                                          └─┘      
st                          └──────────────────┘└─────┘└┘
182  
183  lemma integrable.neg {f : α → β} : integrable f → integrable (λa, -f a) :=
id                                    └────────┘    └────────┘      
src                                     └────────┘     └────────┘      
typ                                   └────────┘    └────────┘      
doc                                     └────────┘     └────────┘
184  assume hfi, calc _ = _ : lintegral_nnnorm_neg
id          └─┘               └──────────────────┘
src                           └──────────────────┘
typ         └─┘               └──────────────────┘
185                   ... < ⊤ : hfi
id                             └─┘
src                         
typ                            └─┘
186  
187  @[simp] lemma integrable_neg_iff (f : α → β) : integrable (λa, -f a) ↔ integrable f :=
id                                                └────────┘         └────────┘ 
src                                                 └────────┘            └────────┘
typ                                               └────────┘         └────────┘ 
doc    └──┘                                         └────────┘              └────────┘
188  begin
st   └─────
189    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
190    { assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
191      simpa only [_root_.neg_neg] using h.neg },
id                   └────────────┘        └───┘
src      └──────────┘└────────────┘└──────┘└───┘
typ      └──────────┘└────────────┘└──────┘└───┘
doc      └──────────┘              └──────┘     
txt      └──────────┘              └──────┘     
par      └──────────┘              └──────┘     
pid           └──┘└┘              └────┘     
st   ───────────────────────────────────────────┘└┘
192    exact integrable.neg
id           └────────────┘
src    └────┘└────────────┘
typ    └────┘└────────────┘
doc    └────┘              
txt    └────┘              
par    └────┘              
pid                       
st   ──────────────────────┘
193  end
st   └─┘
194  
195  lemma integrable.sub {f g : α → β} (hfm : measurable f) (hfi : integrable f) (hgm : measurable g)
id                                           └────────┘          └────────┘          └────────┘ 
src                                            └────────┘           └────────┘           └────────┘
typ                                          └────────┘          └────────┘          └────────┘ 
doc                                            └────────┘           └────────┘           └────────┘
196    (hgi : integrable g) : integrable (λa, f a - g a) :=
id            └────────┘     └────────┘         
src           └────────┘      └────────┘          
typ           └────────┘     └────────┘         
doc           └────────┘      └────────┘
197  by { simp only [sub_eq_add_neg], exact hfi.add hfm (measurable.neg hgm) (integrable.neg hgi) }
id                   └────────────┘         └─────┘ └─┘  └────────────┘ └─┘   └────────────┘ └─┘
src       └─────────┘└────────────┘  └────┘└─────┘    └────────────┘   └┘ └────────────┘   └┘
typ       └─────────┘└────────────┘  └────┘└─────┘└─┘ └────────────┘└─┘└┘ └────────────┘└─┘└┘
doc       └─────────┘                └────┘                            └┘                  └┘
txt       └─────────┘                └────┘                            └┘                  └┘
par       └─────────┘                └────┘                            └┘                  └┘
pid           └──┘└┘                                                 └┘                  
st     └───────────────────────────┘└────────────────────────────────────────────────────────────┘└┘
198  
199  lemma integrable.norm {f : α → β} (hfi : integrable f) : integrable (λa, ∥f a∥) :=
id                                          └────────┘     └────────┘      
src                                           └────────┘      └────────┘         
typ                                         └────────┘     └────────┘      
doc                                           └────────┘      └────────┘
200  have eq : (λa, (nnnorm ∥f a∥ : ennreal)) = λa, (nnnorm (f a) : ennreal),
id                  └────┘     └─────┘        └────┘       └─────┘
src                  └────┘       └─────┘         └────┘         └─────┘
typ                 └────┘     └─────┘        └────┘       └─────┘
doc                  └────┘         └─────┘          └────┘         └─────┘
201    by { funext, rw nnnorm_norm },
id                     └─────────┘
src         └────┘  └─┘└─────────┘
typ         └────┘  └─┘└─────────┘
doc         └────┘  └─┘           
txt         └────┘  └─┘           
par         └────┘  └─┘           
pid                              
st       └───────┘└───────────────┘└┘
202  by { rwa [integrable, eq] }
id             └────────┘  └┘
src       └───┘└────────┘└┘└┘└┘
typ       └───┘└────────┘└┘└┘└┘
doc       └───┘└────────┘└┘  └┘
txt       └───┘          └┘  └┘
par       └───┘          └┘  └┘
pid          └┘          └┘  
st     └────────────────┘└──┘└┘
203  
204  lemma integrable_norm_iff (f : α → β) : integrable (λa, ∥f a∥) ↔ integrable f :=
id                                         └────────┘         └────────┘ 
src                                          └────────┘            └────────┘
typ                                        └────────┘         └────────┘ 
doc                                          └────────┘               └────────┘
205  have eq : (λa, (nnnorm ∥f a∥ : ennreal)) = λa, (nnnorm (f a) : ennreal),
id                  └────┘     └─────┘        └────┘       └─────┘
src                  └────┘       └─────┘         └────┘         └─────┘
typ                 └────┘     └─────┘        └────┘       └─────┘
doc                  └────┘         └─────┘          └────┘         └─────┘
206    by { funext, rw nnnorm_norm },
id                     └─────────┘
src         └────┘  └─┘└─────────┘
typ         └────┘  └─┘└─────────┘
doc         └────┘  └─┘           
txt         └────┘  └─┘           
par         └────┘  └─┘           
pid                              
st       └───────┘└───────────────┘└┘
207  by { rw [integrable, integrable, eq] }
id            └────────┘  └────────┘  └┘
src       └──┘└────────┘└┘└────────┘└┘└┘└┘
typ       └──┘└────────┘└┘└────────┘└┘└┘└┘
doc       └──┘└────────┘└┘└────────┘└┘  └┘
txt       └──┘          └┘          └┘  └┘
par       └──┘          └┘          └┘  └┘
pid         └┘          └┘          └┘  
st     └───────────────┘└──────────┘└──┘└┘
208  
209  lemma integrable_of_integrable_bound {f : α → β} {bound : α → ℝ} (h : integrable bound)
id                                                                     └────────┘ └───┘
src                                                                       └────────┘
typ                                                                    └────────┘ └───┘
doc                                                                        └────────┘
210    (h_bound : ∀ₘ a, ∥f a∥ ≤ bound a) : integrable f :=
id                └┘     └───┘     └────────┘ 
src               └┘                   └────────┘
typ               └┘     └───┘     └────────┘ 
doc               └┘                      └────────┘
211  have h₁ : ∀ₘ a, (nnnorm (f a) : ennreal) ≤ ennreal.of_real (bound a),
id             └┘   └────┘       └─────┘   └─────────────┘  └───┘ 
src            └┘    └────┘         └─────┘   └─────────────┘
typ            └┘   └────┘       └─────┘   └─────────────┘  └───┘ 
doc            └┘    └────┘         └─────┘    └─────────────┘
212  begin
st   └─────
213    filter_upwards [h_bound],
src    └──────────────┘       
typ    └──────────────┘       
doc    └──────────────┘       
txt    └──────────────┘       
par    └──────────────┘       
pid                  └┘       
st   ─────────────────────────┘└─
214    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
215    assume a h,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid    └────────┘
st   ───────────┘└─
216    calc (nnnorm (f a) : ennreal) = ennreal.of_real (∥f a∥) : by rw of_real_norm_eq_coe_nnnorm
id     └──┘  └────┘         └─────┘                                 └────────────────────────┘
src    └──┘  └────┘         └─────┘                               └─┘└────────────────────────┘
typ    └──┘  └────┘         └─────┘                              └─┘└────────────────────────┘
doc    └──┘  └────┘         └─────┘                                 └─┘                          
txt                                                                 └─┘                          
par                                                                 └─┘                          
pid                                                                                             
st   ─────────────────────────────────────────────────────────────┘└──────────────────────────────
217      ... ≤ ennreal.of_real (bound a) : ennreal.of_real_le_of_real h
id             └─────────────┘  └───┘     └────────────────────────┘ 
src  ───┘      └─────────────┘             └────────────────────────┘
typ  ───┘      └─────────────┘  └───┘     └────────────────────────┘ 
doc  ───┘      └─────────────┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└────────────────────────────────────────────────────────────┘
218  end,
st   ──┘
219  calc (∫⁻ a, nnnorm (f a)) ≤ (∫⁻ a, ennreal.of_real (bound a)) :
id         └┘  └────┘         └┘  └─────────────┘  └───┘ 
src        └┘   └────┘           └┘   └─────────────┘
typ        └┘  └────┘         └┘  └─────────────┘  └───┘ 
doc        └┘   └────┘           └┘   └─────────────┘
220      by { apply lintegral_le_lintegral_ae, exact h₁ }
id                  └───────────────────────┘        └┘
src           └────┘└───────────────────────┘  └────┘  
typ           └────┘└───────────────────────┘  └────┘└┘
doc           └────┘                           └────┘  
txt           └────┘                           └────┘  
par           └────┘                           └────┘  
pid                                                  
st         └────────────────────────────────┘└─────────┘└┘
221    ... ≤ (∫⁻ a, ennreal.of_real ∥bound a∥) : lintegral_le_lintegral _ _ $
id            └┘  └─────────────┘ └───┘     └────────────────────┘
src           └┘   └─────────────┘            └────────────────────┘
typ           └┘  └─────────────┘ └───┘     └────────────────────┘
doc           └┘   └─────────────┘
222      by { assume a, apply ennreal.of_real_le_of_real, exact le_max_left (bound a) (-bound a) }
id                            └────────────────────────┘        └─────────┘            └───┘ 
src           └──────┘  └────┘└────────────────────────┘  └────┘└─────────┘       └┘       └┘
typ           └──────┘  └────┘└────────────────────────┘  └────┘└─────────┘       └┘ └───┘└┘
doc           └──────┘  └────┘                            └────┘                  └┘        └┘
txt           └──────┘  └────┘                            └────┘                  └┘        └┘
par           └──────┘  └────┘                            └────┘                  └┘        └┘
pid           └──────┘                                                          └┘        
st         └─────────┘└────────────────────────────────┘└───────────────────────────────────────┘└┘
223    ... < ⊤ : by { rwa [integrable_iff_norm] at h }
id                        └─────────────────┘
src                  └───┘└─────────────────┘└─────┘
typ                  └───┘└─────────────────┘└─────┘
doc                   └───┘                   └─────┘
txt                   └───┘                   └─────┘
par                   └───┘                   └─────┘
pid                      └┘                   └───┘
st                 └─────────────────────────┘└────┘└┘
224  
225  section dominated_convergence
226  
227  variables {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
id                                                     
src                                                    
typ                                                    
228  
229  lemma all_ae_of_real_F_le_bound (h : ∀ n, ∀ₘ a, ∥F n a∥ ≤ bound a) :
id                                            └┘      └───┘ 
src                                            └┘         
typ                                           └┘      └───┘ 
doc                                            └┘  
230    ∀ n, ∀ₘ a, ennreal.of_real ∥F n a∥ ≤ ennreal.of_real (bound a) :=
id         └┘  └─────────────┘     └─────────────┘  └───┘ 
src         └┘   └─────────────┘        └─────────────┘
typ        └┘  └─────────────┘     └─────────────┘  └───┘ 
doc         └┘   └─────────────┘           └─────────────┘
231  λn, by filter_upwards [h n] λ a h, ennreal.of_real_le_of_real h
id                                   └────────────────────────┘
src         └──────────────┘  └┘ └────┘└────────────────────────┘ 
typ        └──────────────┘└┘ └────┘└────────────────────────┘ 
doc         └──────────────┘  └┘ └────┘                           
txt         └──────────────┘  └┘ └────┘                           
par         └──────────────┘  └┘ └────┘                           
pid                       └┘   └────┘                           
st         └─────────────────────────────────────────────────────────
232  
src  
typ  
doc  
txt  
par  
pid  
st   
233  lemma all_ae_tendsto_of_real_norm (h : ∀ₘ a, tendsto (λ n, F n a) at_top $ 𝓝 $ f a) :
id                                          └┘  └─────┘          └────┘       
src                                         └┘   └─────┘              └────┘   
typ                                         └┘  └─────┘          └────┘       
doc                                         └┘   └─────┘              └────┘   
234    ∀ₘ a, tendsto (λn, ennreal.of_real ∥F n a∥) at_top $ 𝓝 $ ennreal.of_real ∥f a∥ :=
id     └┘  └─────┘     └─────────────┘     └────┘      └─────────────┘  
src    └┘   └─────┘      └─────────────┘        └────┘      └─────────────┘    
typ    └┘  └─────┘     └─────────────┘     └────┘      └─────────────┘  
doc    └┘   └─────┘      └─────────────┘          └────┘      └─────────────┘
235  by filter_upwards [h]
src     └──────────────┘ └─
typ     └──────────────┘ └─
doc     └──────────────┘ └─
txt     └──────────────┘ └─
par     └──────────────┘ └─
pid                   └┘ 
st     └───────────────────
236    λ a h, tendsto_of_real $ tendsto.comp (continuous.tendsto continuous_norm _) h
id            └─────────────┘   └──────────┘  └────────────────┘ └─────────────┘
src  ─┘ └────┘└─────────────┘ └──────────┘ └────────────────┘└─────────────┘└──┘ 
typ  ─┘ └────┘└─────────────┘ └──────────┘ └────────────────┘└─────────────┘└──┘ 
doc  ─┘ └────┘                                                              └──┘ 
txt  ─┘ └────┘                                                              └──┘ 
par  ─┘ └────┘                                                              └──┘ 
pid  ─┘ └────┘                                                              └──┘ 
st   ─────────────────────────────────────────────────────────────────────────────────
237  
src  
typ  
doc  
txt  
par  
pid  
st   
238  lemma all_ae_of_real_f_le_bound (h_bound : ∀ n, ∀ₘ a, ∥F n a∥ ≤ bound a)
id                                                  └┘      └───┘ 
src                                                  └┘         
typ                                                 └┘      └───┘ 
doc                                                  └┘  
239    (h_lim : ∀ₘ a, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
id              └┘  └─────┘          └────┘     
src             └┘   └─────┘              └────┘  
typ             └┘  └─────┘          └────┘     
doc             └┘   └─────┘              └────┘  
240    ∀ₘ a, ennreal.of_real ∥f a∥ ≤ ennreal.of_real (bound a) :=
id     └┘  └─────────────┘    └─────────────┘  └───┘ 
src    └┘   └─────────────┘      └─────────────┘
typ    └┘  └─────────────┘    └─────────────┘  └───┘ 
doc    └┘   └─────────────┘         └─────────────┘
241  begin
st   └─────
242    have F_le_bound := all_ae_of_real_F_le_bound h_bound,
id                        └───────────────────────┘ └─────┘
src    └─────────────────┘└───────────────────────┘
typ    └─────────────────┘└───────────────────────┘└─────┘
doc    └─────────────────┘                         
txt    └─────────────────┘                         
par    └─────────────────┘                         
pid    └─────────────┘└─┘                         
st   ─────────────────────────────────────────────────────┘└─
243    rw ← all_ae_all_iff at F_le_bound,
id          └────────────┘
src    └───┘└────────────┘└────────────┘
typ    └───┘└────────────┘└────────────┘
doc    └───┘              └────────────┘
txt    └───┘              └────────────┘
par    └───┘              └────────────┘
pid      └─┘              └────────────┘
st   ──────────────────────────────────┘└─
244    filter_upwards [all_ae_tendsto_of_real_norm h_lim, F_le_bound],
id                     └─────────────────────────┘ └───┘
src    └──────────────┘└─────────────────────────┘     └┘          
typ    └──────────────┘└─────────────────────────┘└───┘└┘          
doc    └──────────────┘                                └┘          
txt    └──────────────┘                                └┘          
par    └──────────────┘                                └┘          
pid                  └┘                                └┘          
st   ───────────────────────────────────────────────────────────────┘└─
245    assume a tendsto_norm F_le_bound,
src    └──────────────────────────────┘
typ    └──────────────────────────────┘
doc    └──────────────────────────────┘
txt    └──────────────────────────────┘
par    └──────────────────────────────┘
pid    └──────────────────────────────┘
st   ─────────────────────────────────┘└─
246    refine le_of_tendsto at_top_ne_bot tendsto_norm _,
id            └───────────┘ └───────────┘ └──────────┘
src    └─────┘└───────────┘└───────────┘            └┘
typ    └─────┘└───────────┘└───────────┘└──────────┘└┘
doc    └─────┘                                      └┘
txt    └─────┘                                      └┘
par    └─────┘                                      └┘
pid                                                └┘
st   ──────────────────────────────────────────────────┘└─
247    simp only [mem_at_top_sets, ge_iff_le, mem_set_of_eq, preimage_set_of_eq, nonempty_of_inhabited],
id                └─────────────┘  └───────┘  └───────────┘  └────────────────┘  └───────────────────┘
src    └─────────┘└─────────────┘└┘└───────┘└┘└───────────┘└┘└────────────────┘└┘└───────────────────┘
typ    └─────────┘└─────────────┘└┘└───────┘└┘└───────────┘└┘└────────────────┘└┘└───────────────────┘
doc    └─────────┘               └┘         └┘             └┘                  └┘                     
txt    └─────────┘               └┘         └┘             └┘                  └┘                     
par    └─────────┘               └┘         └┘             └┘                  └┘                     
pid        └──┘└┘               └┘         └┘             └┘                  └┘                     
st   ─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
248    use 0,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       
st   ──────┘└─
249    assume n hn,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
250    exact F_le_bound n
id           └────────┘ 
src    └────┘           
typ    └────┘└────────┘
doc    └────┘           
txt    └────┘           
par    └────┘           
pid                    
st   ────────────────────┘
251  end
st   └─┘
252  
253  lemma integrable_of_dominated_convergence {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
id                                                                                
src                                                                                    
typ                                                                               
254    (bound_integrable : integrable bound)
id                         └────────┘ └───┘
src                        └────────┘
typ                        └────────┘ └───┘
doc                        └────────┘
255    (h_bound : ∀ n, ∀ₘ a, ∥F n a∥ ≤ bound a)
id                    └┘      └───┘ 
src                    └┘         
typ                   └┘      └───┘ 
doc                    └┘  
256    (h_lim : ∀ₘ a, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
id              └┘  └─────┘          └────┘     
src             └┘   └─────┘              └────┘  
typ             └┘  └─────┘          └────┘     
doc             └┘   └─────┘              └────┘  
257    integrable f :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
258  /- `∥F n a∥ ≤ bound a` and `∥F n a∥ --> ∥f a∥` implies `∥f a∥ ≤ bound a`,
259    and so `∫ ∥f∥ ≤ ∫ bound < ⊤` since `bound` is integrable -/
260  begin
st   └─────
261    rw integrable_iff_norm,
id        └─────────────────┘
src    └─┘└─────────────────┘
typ    └─┘└─────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────────────┘└─
262    calc (∫⁻ a, (ennreal.of_real ∥f a∥)) ≤ ∫⁻ a, ennreal.of_real (bound a) :
id     └──┘  └┘                               └─────────────┘  └───┘
src    └──┘  └┘                                  └─────────────┘
typ    └──┘  └┘                               └─────────────┘  └───┘
doc    └──┘  └┘                                    └─────────────┘
st   ───────────────────────────────────────────────────────────────────────────
263      lintegral_le_lintegral_ae $ all_ae_of_real_f_le_bound h_bound h_lim
id       └───────────────────────┘   └───────────────────────┘ └─────┘ └───┘
src      └───────────────────────┘   └───────────────────────┘
typ      └───────────────────────┘   └───────────────────────┘ └─────┘ └───┘
st   ────────────────────────────────────────────────────────────────────────
264      ... < ⊤ :
id             
src            
typ            
st   ──────────────
265      begin
st   ───┘└─────
266        rw ← integrable_iff_of_real,
id              └────────────────────┘
src        └───┘└────────────────────┘
typ        └───┘└────────────────────┘
doc        └───┘
txt        └───┘
par        └───┘
pid          └─┘
st   ────────────────────────────────┘└─
267        { exact bound_integrable },
id                 └──────────────┘
src          └────┘                
typ          └────┘└──────────────┘
doc          └────┘                
txt          └────┘                
par          └────┘                
pid                               
st   ───────┘└─────────────────────┘└┘
268        filter_upwards [h_bound 0] λ a h, le_trans (norm_nonneg _) h,
id                         └─────┘           └──────┘  └─────────┘
src        └──────────────┘       └──┘ └────┘└──────┘ └─────────┘└──┘
typ        └──────────────┘└─────┘└──┘ └────┘└──────┘ └─────────┘└──┘
doc        └──────────────┘       └──┘ └────┘                    └──┘
txt        └──────────────┘       └──┘ └────┘                    └──┘
par        └──────────────┘       └──┘ └────┘                    └──┘
pid                      └┘       └─┘ └────┘                    └──┘
st   ─────────────────────────────────────────────────────────────────┘└─
269      end
st   ────────
270  end
st   ──┘
271  
272  lemma tendsto_lintegral_norm_of_dominated_convergence [second_countable_topology β]
id                                                          └───────────────────────┘ 
src                                                         └───────────────────────┘
typ                                                         └───────────────────────┘ 
doc                                                         └───────────────────────┘
273    {F : ℕ → α → β} {f : α → β} {bound : α → ℝ}
id                                        
src                                            
typ                                       
274    (F_measurable : ∀ n, measurable (F n))
id                         └────────┘   
src                         └────────┘
typ                        └────────┘   
doc                         └────────┘
275    (f_measurable : measurable f)
id                     └────────┘ 
src                    └────────┘
typ                    └────────┘ 
doc                    └────────┘
276    (bound_integrable : integrable bound)
id                         └────────┘ └───┘
src                        └────────┘
typ                        └────────┘ └───┘
doc                        └────────┘
277    (h_bound : ∀ n, ∀ₘ a, ∥F n a∥ ≤ bound a)
id                    └┘      └───┘ 
src                    └┘         
typ                   └┘      └───┘ 
doc                    └┘  
278    (h_lim : ∀ₘ a, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
id              └┘  └─────┘          └────┘     
src             └┘   └─────┘              └────┘  
typ             └┘  └─────┘          └────┘     
doc             └┘   └─────┘              └────┘  
279    tendsto (λn, ∫⁻ a, ennreal.of_real ∥F n a - f a∥) at_top (𝓝 0) :=
id     └─────┘     └┘  └─────────────┘        └────┘  
src    └─────┘      └┘   └─────────────┘             └────┘  
typ    └─────┘     └┘  └─────────────┘        └────┘  
doc    └─────┘      └┘   └─────────────┘                └────┘  
280  let b := λa, 2 * ennreal.of_real (bound a) in
id                 └─────────────┘  └───┘ 
src                  └─────────────┘
typ                └─────────────┘  └───┘ 
doc                   └─────────────┘
281  /- `∥F n a∥ ≤ bound a` and `F n a --> f a` implies `∥f a∥ ≤ bound a`, and thus by the
282    triangle inequality, have `∥F n a - f a∥ ≤ 2 * (bound a). -/
283  have hb : ∀ n, ∀ₘ a, ennreal.of_real ∥F n a - f a∥ ≤ b a,
id                 └┘  └─────────────┘         
src                 └┘   └─────────────┘            
typ                └┘  └─────────────┘         
doc                 └┘   └─────────────┘
284  begin
st   └─────
285    assume n,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
286    filter_upwards [all_ae_of_real_F_le_bound h_bound n, all_ae_of_real_f_le_bound h_bound h_lim],
id                     └───────────────────────┘ └─────┘   └───────────────────────┘ └─────┘ └───┘
src    └──────────────┘└───────────────────────┘        └┘└───────────────────────┘            
typ    └──────────────┘└───────────────────────┘└─────┘└┘└───────────────────────┘└─────┘└───┘
doc    └──────────────┘                                 └┘                                     
txt    └──────────────┘                                 └┘                                     
par    └──────────────┘                                 └┘                                     
pid                  └┘                                 └┘                                     
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
287    assume a h₁ h₂,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid    └────────────┘
st   ───────────────┘└─
288    calc ennreal.of_real ∥F n a - f a∥ ≤ (ennreal.of_real ∥F n a∥) + (ennreal.of_real ∥f a∥) :
id     └──┘                                                         └─────────────┘   
src    └──┘                                                           └─────────────┘
typ    └──┘                                                         └─────────────┘   
doc    └──┘                                                              └─────────────┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────
289    begin
st   ─┘└─────
290      rw [← ennreal.of_real_add],
id             └─────────────────┘
src      └────┘└─────────────────┘
typ      └────┘└─────────────────┘
doc      └────┘                   
txt      └────┘                   
par      └────┘                   
pid        └──┘                   
st   ────────────────────────────┘└──
291      apply of_real_le_of_real,
id             └────────────────┘
src      └────┘└────────────────┘
typ      └────┘└────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────────────┘└─
292      { apply norm_sub_le }, { exact norm_nonneg _ }, { exact norm_nonneg _ }
id               └─────────┘            └─────────┘              └─────────┘
src        └────┘└─────────┘     └────┘└─────────┘└─┘     └────┘└─────────┘└─┘
typ        └────┘└─────────┘     └────┘└─────────┘└─┘     └────┘└─────────┘└─┘
doc        └────┘                └────┘           └─┘     └────┘           └─┘
txt        └────┘                └────┘           └─┘     └────┘           └─┘
par        └────┘                └────┘           └─┘     └────┘           └─┘
pid                                             └┘                     └┘
st   ─────┘└────────────────┘└┘└─┘└──────────────────┘└┘└─────────────────────┘└─
293    end
st   ────┘
294      ... ≤ (ennreal.of_real (bound a)) + (ennreal.of_real (bound a)) : add_le_add' h₁ h₂
id                                                            └───┘       └─────────┘ └┘ └┘
src                                                                       └─────────┘
typ                                                           └───┘       └─────────┘ └┘ └┘
st   ────────────────────────────────────────────────────────────────────────────────────────
295      ... = b a : by rw ← two_mul
id                          └─────┘
src                     └───┘└─────┘
typ                    └───┘└─────┘
doc                     └───┘       
txt                     └───┘       
par                     └───┘       
pid                       └─┘       
st   ─────────────────┘└────────────┘
296  end,
st   └─┘
297  /- On the other hand, `F n a --> f a` implies that `∥F n a - f a∥ --> 0`  -/
298  have h : ∀ₘ a, tendsto (λ n, ennreal.of_real ∥F n a - f a∥) at_top (𝓝 0),
id            └┘  └─────┘      └─────────────┘        └────┘  
src           └┘   └─────┘       └─────────────┘             └────┘  
typ           └┘  └─────┘      └─────────────┘        └────┘  
doc           └┘   └─────┘       └─────────────┘                └────┘  
299  begin
st   └─────
300    suffices h : ∀ₘ a, tendsto (λ n, ennreal.of_real ∥F n a - f a∥) at_top (𝓝 $ ennreal.of_real 0),
id                  └┘   └─────┘                                    └────┘     └─────────────┘
src    └───────────┘└┘└┘└─────┘  └──┘                       └┘└────┘  └─────────────┘└─┘
typ    └───────────┘└┘└┘└─────┘  └──┘                     └┘└────┘  └─────────────┘└─┘
doc    └───────────┘└┘└┘└─────┘  └──┘                       └┘└────┘  └─────────────┘└─┘
txt    └───────────┘  └┘          └──┘                       └┘                        └─┘
par    └───────────┘  └┘          └──┘                       └┘                        └─┘
pid    └────────┘└─┘  └┘          └──┘                       └┘                        └─┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
301    { rwa ennreal.of_real_zero at h },
id           └──────────────────┘
src      └──┘└──────────────────┘└────┘
typ      └──┘└──────────────────┘└────┘
doc      └──┘                    └────┘
txt      └──┘                    └────┘
par      └──┘                    └────┘
pid                             └───┘
st   ───┘└────────────────────────────┘└┘
302    filter_upwards [h_lim],
src    └──────────────┘     
typ    └──────────────┘     
doc    └──────────────┘     
txt    └──────────────┘     
par    └──────────────┘     
pid                  └┘     
st   ───────────────────────┘└─
303    assume a h,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid    └────────┘
st   ───────────┘└─
304    refine tendsto.comp (continuous.tendsto continuous_of_real _) _,
id            └──────────┘  └────────────────┘ └────────────────┘
src    └─────┘└──────────┘ └────────────────┘└────────────────┘└───┘
typ    └─────┘└──────────┘ └────────────────┘└────────────────┘└───┘
doc    └─────┘                                                 └───┘
txt    └─────┘                                                 └───┘
par    └─────┘                                                 └───┘
pid                                                           └───┘
st   ────────────────────────────────────────────────────────────────┘└─
305    rw ← tendsto_iff_norm_tendsto_zero,
id          └───────────────────────────┘
src    └───┘└───────────────────────────┘
typ    └───┘└───────────────────────────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ───────────────────────────────────┘└─
306    exact h
id           
src    └────┘ 
typ    └────┘
doc    └────┘ 
txt    └────┘ 
par    └────┘ 
pid          
st   ─────────┘
307  end,
st   └─┘
308  /- Therefore, by the dominated convergence theorem for nonnegative integration, have
309    ` ∫ ∥f a - F n a∥ --> 0 ` -/
310  begin
st   └─────
311    suffices h : tendsto (λn, ∫⁻ a, ennreal.of_real ∥F n a - f a∥) at_top (𝓝 (∫⁻ (a:α), 0)),
id                  └─────┘            └─────────────┘              └────┘     └┘     
src    └───────────┘└─────┘  └─┘  └┘ └─────────────┘        └┘└────┘   └┘└──┘ └──┘
typ    └───────────┘└─────┘  └─┘  └┘ └─────────────┘      └┘└────┘   └┘└──┘└──┘
doc    └───────────┘└─────┘  └─┘  └┘ └─────────────┘        └┘└────┘   └┘└──┘ └──┘
txt    └───────────┘         └─┘  └┘                        └┘           └──┘  └──┘
par    └───────────┘         └─┘  └┘                        └┘           └──┘  └──┘
pid    └────────┘└─┘         └─┘  └┘                        └┘           └──┘  └──┘
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
312    { rwa lintegral_zero at h },
id           └────────────┘
src      └──┘└────────────┘└────┘
typ      └──┘└────────────┘└────┘
doc      └──┘              └────┘
txt      └──┘              └────┘
par      └──┘              └────┘
pid                       └───┘
st   ───┘└──────────────────────┘└┘
313    -- Using the dominated convergence theorem.
st   ──────────────────────────────────────────────
314    refine tendsto_lintegral_of_dominated_convergence _ _ hb _ _,
id            └────────────────────────────────────────┘     └┘
src    └─────┘└────────────────────────────────────────┘└───┘  └──┘
typ    └─────┘└────────────────────────────────────────┘└───┘└┘└──┘
doc    └─────┘└────────────────────────────────────────┘└───┘  └──┘
txt    └─────┘                                          └───┘  └──┘
par    └─────┘                                          └───┘  └──┘
pid                                                    └───┘  └──┘
st   ─────────────────────────────────────────────────────────────┘└─
315    -- Show `λa, ∥f a - F n a∥` is measurable for all `n`
st   ────────────────────────────────────────────────────────
316    { exact λn, measurable.comp measurable_of_real (measurable.norm (measurable.sub (F_measurable n)
id                 └─────────────┘ └────────────────┘  └─────────────┘  └────────────┘  └──────────┘
src      └────┘ └─┘└─────────────┘└────────────────┘ └─────────────┘ └────────────┘              └─
typ      └────┘ └─┘└─────────────┘└────────────────┘ └─────────────┘ └────────────┘ └──────────┘ └─
doc      └────┘ └─┘                                                                              └─
txt      └────┘ └─┘                                                                              └─
par      └────┘ └─┘                                                                              └─
pid            └─┘                                                                              └─
st   ───┘└──────────────────────────────────────────────────────────────────────────────────────────────
317        f_measurable)) },
id         └──────────┘
src  ─────┘            └─┘
typ  ─────┘└──────────┘└─┘
doc  ─────┘            └─┘
txt  ─────┘            └─┘
par  ─────┘            └─┘
pid  ─────┘            └┘
st   ────────────────────┘└┘
318    -- Show `2 * bound` is integrable
st   ────────────────────────────────────
319    { rw integrable_iff_of_real at bound_integrable,
id          └────────────────────┘
src      └─┘└────────────────────┘└──────────────────┘
typ      └─┘└────────────────────┘└──────────────────┘
doc      └─┘                      └──────────────────┘
txt      └─┘                      └──────────────────┘
par      └─┘                      └──────────────────┘
pid                              └──────────────────┘
st   ───┘└───────────────────────────────────────────┘└─
320      { calc (∫⁻ a, b a) = 2 * (∫⁻ a, ennreal.of_real (bound a)) :
id         └──┘                      └─────────────┘  └───┘
src        └──┘                         └─────────────┘
typ        └──┘                      └─────────────┘  └───┘
doc        └──┘                          └─────────────┘
st   ─────┘└──────────────────────────────────────────────────────────
321          by { rw lintegral_const_mul', exact coe_ne_top }
id                   └──────────────────┘        └────────┘
src               └─┘└──────────────────┘  └────┘└────────┘
typ               └─┘└──────────────────┘  └────┘└────────┘
doc               └─┘                      └────┘          
txt               └─┘                      └────┘          
par               └─┘                      └────┘          
pid                                                      
st   ─────────┘└────────────────────────┘└─────────────────┘└┘
322          ... < ⊤ : mul_lt_top (coe_lt_top) bound_integrable },
id                    └────────┘  └────────┘  └──────────────┘
src                   └────────┘  └────────┘
typ                   └────────┘  └────────┘  └──────────────┘
st   └────────────────────────────────────────────────────────┘└─┘
323      filter_upwards [h_bound 0] λ a h, le_trans (norm_nonneg _) h },
id                       └─────┘           └──────┘  └─────────┘
src      └──────────────┘       └──┘ └────┘└──────┘ └─────────┘└──┘ 
typ      └──────────────┘└─────┘└──┘ └────┘└──────┘ └─────────┘└──┘ 
doc      └──────────────┘       └──┘ └────┘                    └──┘ 
txt      └──────────────┘       └──┘ └────┘                    └──┘ 
par      └──────────────┘       └──┘ └────┘                    └──┘ 
pid                    └┘       └─┘ └────┘                    └──┘ 
st   ────────────────────────────────────────────────────────────────┘└┘
324    -- Show `∥f a - F n a∥ --> 0`
st   ────────────────────────────────
325    { exact h }
id             
src      └────┘ 
typ      └────┘
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid            
st   ───────────┘└─
326  end
st   ──┘
327  
328  end dominated_convergence
329  
330  section pos_part
331  /-! Lemmas used for defining the positive part of a `L¹` function -/
332  
333  lemma integrable.max_zero {f : α → ℝ} (hf : integrable f) : integrable (λa, max (f a) 0) :=
id                                             └────────┘     └────────┘     └─┘   
src                                             └────────┘      └────────┘      └─┘
typ                                            └────────┘     └────────┘     └─┘   
doc                                              └────────┘      └────────┘
334  begin
st   └─────
335    simp only [integrable_iff_norm] at *,
id                └─────────────────┘
src    └─────────┘└─────────────────┘└────┘
typ    └─────────┘└─────────────────┘└────┘
doc    └─────────┘                   └────┘
txt    └─────────┘                   └────┘
par    └─────────┘                   └────┘
pid        └──┘└┘                   └──┘
st   ─────────────────────────────────────┘└─
336    calc (∫⁻ a, ennreal.of_real ∥max (f a) 0∥) ≤ (∫⁻ (a : α), ennreal.of_real ∥f a∥) :
id     └──┘  └┘                  └─┘                        └─────────────┘  
src    └──┘  └┘                   └─┘                         └─────────────┘
typ    └──┘  └┘                  └─┘                        └─────────────┘  
doc    └──┘  └┘                                                 └─────────────┘
st   ─────────────────────────────────────────────────────────────────────────────────────
337      lintegral_le_lintegral _ _
id       └────────────────────┘
src      └────────────────────┘
typ      └────────────────────┘
st   ───────────────────────────────
338      begin
st   ───┘└─────
339        assume a,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────────────┘└─
340        apply of_real_le_of_real,
id               └────────────────┘
src        └────┘└────────────────┘
typ        └────┘└────────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────────────┘└─
341        simp only [real.norm_eq_abs],
id                    └──────────────┘
src        └─────────┘└──────────────┘
typ        └─────────┘└──────────────┘
doc        └─────────┘                
txt        └─────────┘                
par        └─────────┘                
pid            └──┘└┘                
st   ─────────────────────────────────┘└─
342        calc abs (max (f a) 0) = max (f a) 0 : by { rw abs_of_nonneg, apply le_max_right }
id                                  └─┘                   └───────────┘        └──────────┘
src                                 └─┘                └─┘└───────────┘  └────┘└──────────┘
typ                                 └─┘                └─┘└───────────┘  └────┘└──────────┘
doc                                                    └─┘               └────┘            
txt                                                    └─┘               └────┘            
par                                                    └─┘               └────┘            
pid                                                                                      
st   ──────────────────────────────────────────────┘└─────────────────┘└───────────────────┘└┘
343          ... ≤ abs (f a) : max_le (le_abs_self _) (abs_nonneg _)
id                 └─┘       └────┘  └─────────┘     └────────┘
src                └─┘         └────┘  └─────────┘     └────────┘
typ                └─┘       └────┘  └─────────┘     └────────┘
st   └─────────────────────────────────────────────────────────────┘
344      end
st   ──────┘
345      ... < ⊤ : hf
id                └┘
src            
typ               └┘
st   ───────────────┘
346  end
st   ──┘
347  
348  lemma integrable.min_zero {f : α → ℝ} (hf : integrable f) : integrable (λa, min (f a) 0) :=
id                                             └────────┘     └────────┘     └─┘   
src                                             └────────┘      └────────┘      └─┘
typ                                            └────────┘     └────────┘     └─┘   
doc                                              └────────┘      └────────┘
349  begin
st   └─────
350    have : (λa, min (f a) 0) = (λa, - max (-f a) 0),
id                 └─┘                  └─┘  
src    └─────┘  └─┘└─┘   └───┘  └─┘ └─┘   └──┘
typ    └─────┘  └─┘└─┘   └───┘  └─┘ └─┘  └──┘
doc    └─────┘  └─┘      └───┘   └─┘        └──┘
txt    └─────┘  └─┘      └───┘   └─┘        └──┘
par    └─────┘  └─┘      └───┘   └─┘        └──┘
pid    └───┘└┘  └─┘      └───┘   └─┘        └──┘
st   ────────────────────────────────────────────────┘└─
351    { funext, rw [min_eq_neg_max_neg_neg, neg_zero] },
id                   └────────────────────┘  └──────┘
src      └────┘  └──┘└────────────────────┘└┘└──────┘└┘
typ      └────┘  └──┘└────────────────────┘└┘└──────┘└┘
doc      └────┘  └──┘                      └┘        └┘
txt      └────┘  └──┘                      └┘        └┘
par      └────┘  └──┘                      └┘        └┘
pid                └┘                      └┘        
st   ───┘└────┘└──────────────────────────┘└────────┘└┘
352    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
353    exact (integrable.max_zero hf.neg).neg,
id            └─────────────────┘ └────┘
src    └────┘ └─────────────────┘└────┘└───┘
typ    └────┘ └─────────────────┘└────┘└───┘
doc    └────┘                          └───┘
txt    └────┘                          └───┘
par    └────┘                          └───┘
pid                                   └──┘
st   ───────────────────────────────────────┘└─
354  end
st   ──┘
355  
356  end pos_part
357  
358  section normed_space
359  variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id                          └──────────┘     └──────────┘
src                         └──────────┘     └──────────┘
typ                         └──────────┘     └──────────┘
doc                         └──────────┘     └──────────┘
360  
361  lemma integrable.smul (c : 𝕜) {f : α → β} : integrable f → integrable (λa, c • f a) :=
id                                            └────────┘    └────────┘        
src                                              └────────┘     └────────┘        
typ                                           └────────┘    └────────┘        
doc                                              └────────┘     └────────┘
362  begin
st   └─────
363    simp only [integrable], assume hfi,
id                └────────┘
src    └─────────┘└────────┘  └────────┘
typ    └─────────┘└────────┘  └────────┘
doc    └─────────┘└────────┘  └────────┘
txt    └─────────┘            └────────┘
par    └─────────┘            └────────┘
pid        └──┘└┘            └────────┘
st   ───────────────────────┘└──────────┘└─
364    calc
id     └──┘
src    └──┘
typ    └──┘
doc    └──┘
st   ───────
365      (∫⁻ (a : α), nnnorm ((c • f) a)) = (∫⁻ (a : α), (nnnorm c) * nnnorm (f a)) :
id        └┘                                                     └────┘  
src       └┘                                                       └────┘
typ       └┘                                                     └────┘  
doc       └┘                                                         └────┘
st   ─────────────────────────────────────────────────────────────────────────────────
366      begin
st   ───┘└─────
367        apply lintegral_congr_ae,
id               └────────────────┘
src        └────┘└────────────────┘
typ        └────┘└────────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────────────┘└─
368        filter_upwards [],
src        └───────────────┘
typ        └───────────────┘
doc        └───────────────┘
txt        └───────────────┘
par        └───────────────┘
pid                      └─┘
st   ──────────────────────┘└─
369        assume a,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────────────┘└─
370        simp only [nnnorm_smul, set.mem_set_of_eq, pi.smul_apply, ennreal.coe_mul]
id                    └─────────┘  └───────────────┘  └───────────┘  └─────────────┘
src        └─────────┘└─────────┘└┘└───────────────┘└┘└───────────┘└┘└─────────────┘└─
typ        └─────────┘└─────────┘└┘└───────────────┘└┘└───────────┘└┘└─────────────┘└─
doc        └─────────┘           └┘                 └┘             └┘               └─
txt        └─────────┘           └┘                 └┘             └┘               └─
par        └─────────┘           └┘                 └┘             └┘               └─
pid            └──┘└┘           └┘                 └┘             └┘               
st   ─────────────────────────────────────────────────────────────────────────────────
371      end
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
372      ... < ⊤ :
id             
src            
typ            
st   ──────────────
373      begin
st   ───┘└─────
374        rw lintegral_const_mul',
id            └──────────────────┘
src        └─┘└──────────────────┘
typ        └─┘└──────────────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ────────────────────────────┘└─
375        apply mul_lt_top,
id               └────────┘
src        └────┘└────────┘
typ        └────┘└────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────┘└─
376        { exact coe_lt_top },
id                 └────────┘
src          └────┘└────────┘
typ          └────┘└────────┘
doc          └────┘          
txt          └────┘          
par          └────┘          
pid                         
st   ───────┘└───────────────┘└┘
377        { exact hfi },
id                 └─┘
src          └────┘   
typ          └────┘└─┘
doc          └────┘   
txt          └────┘   
par          └────┘   
pid                  
st   ───────┘└────────┘└┘
378        { simp only [ennreal.coe_ne_top, ne.def, not_false_iff] }
id                      └────────────────┘  └────┘  └───────────┘
src          └─────────┘└────────────────┘└┘└────┘└┘└───────────┘└┘
typ          └─────────┘└────────────────┘└┘└────┘└┘└───────────┘└┘
doc          └─────────┘                  └┘      └┘             └┘
txt          └─────────┘                  └┘      └┘             └┘
par          └─────────┘                  └┘      └┘             └┘
pid              └──┘└┘                  └┘      └┘             
st   ─────────────────────────────────────────────────────────────┘└─
379      end
st   ────────
380  end
st   ──┘
381  
382  lemma integrable_smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) : integrable (λa, c • f a) ↔ integrable f :=
id                                                           └────────┘           └────────┘ 
src                                                              └────────┘               └────────┘
typ                                                          └────────┘           └────────┘ 
doc                                                               └────────┘                 └────────┘
383  begin
st   └─────
384    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
385    { assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
386      simpa only [smul_smul, inv_mul_cancel hc, one_smul] using h.smul c⁻¹ },
id                   └───────┘  └────────────┘ └┘  └──────┘        └────┘ └┘
src      └──────────┘└───────┘└┘└────────────┘  └┘└──────┘└──────┘└────┘ └┘
typ      └──────────┘└───────┘└┘└────────────┘└┘└┘└──────┘└──────┘└────┘└┘
doc      └──────────┘         └┘                └┘        └──────┘         
txt      └──────────┘         └┘                └┘        └──────┘         
par      └──────────┘         └┘                └┘        └──────┘         
pid           └──┘└┘         └┘                └┘        └────┘         
st   ────────────────────────────────────────────────────────────────────────┘└┘
387    exact integrable.smul _
id           └─────────────┘
src    └────┘└─────────────┘└─┘
typ    └────┘└─────────────┘└─┘
doc    └────┘               └─┘
txt    └────┘               └─┘
par    └────┘               └─┘
pid                        └┘
st   ─────────────────────────┘
388  end
st   └─┘
389  
390  end normed_space
391  
392  variables [second_countable_topology β]
id              └───────────────────────┘
src             └───────────────────────┘
typ             └───────────────────────┘
doc             └───────────────────────┘
393  
394  namespace ae_eq_fun
395  
396  /-- An almost everywhere equal function is `integrable` if it has a finite distance to the origin.
397    Should mean the same thing as the predicate `integrable` over functions. -/
398  def integrable (f : α →ₘ β) : Prop := f ∈ ball (0 : α →ₘ β) ⊤
id                        └┘               └──┘       └┘   
src                        └┘                 └──┘        └┘    
typ                       └┘               └──┘       └┘   
doc                        └┘                  └──┘        └┘
399  
400  lemma integrable_mk (f : α → β) (hf : measurable f) :
id                                       └────────┘ 
src                                        └────────┘
typ                                      └────────┘ 
doc                                        └────────┘
401    (integrable (mk f hf)) ↔ measure_theory.integrable f :=
id      └────────┘  └┘  └┘    └───────────────────────┘ 
src     └────────┘  └┘         └───────────────────────┘
typ     └────────┘  └┘  └┘    └───────────────────────┘ 
doc     └────────┘  └┘          └───────────────────────┘
402  by simp [integrable, zero_def, edist_mk_mk', measure_theory.integrable, nndist_eq_nnnorm]
id            └────────┘  └──────┘  └──────────┘  └───────────────────────┘  └──────────────┘
src     └────┘└────────┘└┘└──────┘└┘└──────────┘└┘└───────────────────────┘└┘└──────────────┘└─
typ     └────┘└────────┘└┘└──────┘└┘└──────────┘└┘└───────────────────────┘└┘└──────────────┘└─
doc     └────┘└────────┘└┘        └┘            └┘└───────────────────────┘└┘                └─
txt     └────┘          └┘        └┘            └┘                         └┘                └─
par     └────┘          └┘        └┘            └┘                         └┘                └─
pid                   └┘        └┘            └┘                         └┘                
st     └───────────────────────────────────────────────────────────────────────────────────────
403  
src  
typ  
doc  
txt  
par  
pid  
st   
404  lemma integrable_to_fun (f : α →ₘ β) : integrable f ↔ (measure_theory.integrable f.to_fun) :=
id                                 └┘     └────────┘    └───────────────────────┘ └─────┘
src                                 └┘      └────────┘     └───────────────────────┘  └─────┘
typ                                └┘     └────────┘    └───────────────────────┘ └─────┘
doc                                 └┘      └────────┘      └───────────────────────┘  └─────┘
405  by conv_lhs { rw [self_eq_mk f, integrable_mk] }
id                     └────────┘   └───────────┘
src     └─────────┘└──┘└────────┘ └┘└───────────┘└┘└─
typ     └─────────┘└──┘└────────┘└┘└───────────┘└┘└─
txt     └─────────┘└──┘           └┘             └┘└─
par     └─────────┘└──┘           └┘             └┘└─
pid             └────┘           └┘             └─┘
st     └─────────┘└───────────────┘└─────────────┘ 
406  
src  
typ  
txt  
par  
pid  
st   
407  local attribute [simp] integrable_mk
id                          └───────────┘
src                         └───────────┘
typ                         └───────────┘
doc                   └──┘
408  
409  lemma integrable_zero : integrable (0 : α →ₘ β) := mem_ball_self coe_lt_top
id                           └────────┘       └┘      └───────────┘ └────────┘
src                          └────────┘        └┘       └───────────┘ └────────┘
typ                          └────────┘       └┘      └───────────┘ └────────┘
doc                          └────────┘        └┘
410  
411  lemma integrable.add : ∀ {f g : α →ₘ β}, integrable f → integrable g → integrable (f + g) :=
id                                    └┘    └────────┘    └────────┘    └────────┘    
src                                    └┘     └────────┘     └────────┘     └────────┘    
typ                                   └┘    └────────┘    └────────┘    └────────┘    
doc                                    └┘     └────────┘     └────────┘     └────────┘
412  begin
st   └─────
413    rintros ⟨f, hf⟩ ⟨g, hg⟩,
src    └─────────────────────┘
typ    └─────────────────────┘
doc    └─────────────────────┘
txt    └─────────────────────┘
par    └─────────────────────┘
pid           └──────────────┘
st   ────────────────────────┘└─
414    simp only [mem_ball, zero_def, mk_add_mk, integrable_mk, quot_mk_eq_mk],
id                └──────┘  └──────┘  └───────┘  └───────────┘  └───────────┘
src    └─────────┘└──────┘└┘└──────┘└┘└───────┘└┘└───────────┘└┘└───────────┘
typ    └─────────┘└──────┘└┘└──────┘└┘└───────┘└┘└───────────┘└┘└───────────┘
doc    └─────────┘        └┘        └┘         └┘             └┘             
txt    └─────────┘        └┘        └┘         └┘             └┘             
par    └─────────┘        └┘        └┘         └┘             └┘             
pid        └──┘└┘        └┘        └┘         └┘             └┘             
st   ────────────────────────────────────────────────────────────────────────┘└─
415    assume hfi hgi,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid    └────────────┘
st   ───────────────┘└─
416    exact hfi.add hf hg hgi
id           └─────┘ └┘ └┘ └─┘
src    └────┘└─────┘       
typ    └────┘└─────┘└┘└┘└─┘
doc    └────┘              
txt    └────┘              
par    └────┘              
pid                       
st   ─────────────────────────┘
417  end
st   └─┘
418  
419  lemma integrable.neg : ∀ {f : α →ₘ β}, integrable f → integrable (-f) :=
id                                  └┘    └────────┘    └────────┘  
src                                  └┘     └────────┘     └────────┘  
typ                                 └┘    └────────┘    └────────┘  
doc                                  └┘     └────────┘     └────────┘
420  by { rintros ⟨f, hf⟩, have := measure_theory.integrable.neg, simpa }
id                                 └───────────────────────────┘
src       └─────────────┘  └──────┘└───────────────────────────┘  └────┘
typ       └─────────────┘  └──────┘└───────────────────────────┘  └────┘
doc       └─────────────┘  └──────┘                               └────┘
txt       └─────────────┘  └──────┘                               └────┘
par       └─────────────┘  └──────┘                               └────┘
pid              └──────┘  └───┘└─┘                                    
st     └────────────────┘└─────────────────────────────────────┘└──────┘└┘
421  
422  lemma integrable.sub : ∀ {f g : α →ₘ β}, integrable f → integrable g → integrable (f - g) :=
id                                    └┘    └────────┘    └────────┘    └────────┘    
src                                    └┘     └────────┘     └────────┘     └────────┘    
typ                                   └┘    └────────┘    └────────┘    └────────┘    
doc                                    └┘     └────────┘     └────────┘     └────────┘
423  begin
st   └─────
424    rintros ⟨f, hfm⟩ ⟨g, hgm⟩,
src    └───────────────────────┘
typ    └───────────────────────┘
doc    └───────────────────────┘
txt    └───────────────────────┘
par    └───────────────────────┘
pid           └────────────────┘
st   ──────────────────────────┘└─
425    simp only [mem_ball, zero_def, mk_sub_mk, integrable_mk, quot_mk_eq_mk],
id                └──────┘  └──────┘  └───────┘  └───────────┘  └───────────┘
src    └─────────┘└──────┘└┘└──────┘└┘└───────┘└┘└───────────┘└┘└───────────┘
typ    └─────────┘└──────┘└┘└──────┘└┘└───────┘└┘└───────────┘└┘└───────────┘
doc    └─────────┘        └┘        └┘         └┘             └┘             
txt    └─────────┘        └┘        └┘         └┘             └┘             
par    └─────────┘        └┘        └┘         └┘             └┘             
pid        └──┘└┘        └┘        └┘         └┘             └┘             
st   ────────────────────────────────────────────────────────────────────────┘└─
426    assume hfi hgi,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid    └────────────┘
st   ───────────────┘└─
427    exact hfi.sub hfm hgm hgi
id           └─────┘ └─┘ └─┘ └─┘
src    └────┘└─────┘         
typ    └────┘└─────┘└─┘└─┘└─┘
doc    └────┘                
txt    └────┘                
par    └────┘                
pid                         
st   ───────────────────────────┘
428  end
st   └─┘
429  
430  protected lemma is_add_subgroup : is_add_subgroup (ball (0 : α →ₘ β) ⊤) :=
id                                     └─────────────┘  └──┘       └┘   
src                                    └─────────────┘  └──┘        └┘    
typ                                    └─────────────┘  └──┘       └┘   
doc                                    └─────────────┘  └──┘        └┘
431  { zero_mem := integrable_zero,
id                 └─────────────┘
src                └─────────────┘
typ                └─────────────┘
432    add_mem := λ _ _, integrable.add,
id                     └────────────┘
src                      └────────────┘
typ                    └────────────┘
433    neg_mem := λ _, integrable.neg }
id                    └────────────┘
src                    └────────────┘
typ                   └────────────┘
434  
435  section normed_space
436  variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id                          └──────────┘     └──────────┘
src                         └──────────┘     └──────────┘
typ                         └──────────┘     └──────────┘
doc                         └──────────┘     └──────────┘
437  
438  lemma integrable.smul : ∀ {c : 𝕜} {f : α →ₘ β}, integrable f → integrable (c • f) :=
id                                          └┘    └────────┘    └────────┘    
src                                           └┘     └────────┘     └────────┘    
typ                                         └┘    └────────┘    └────────┘    
doc                                           └┘     └────────┘     └────────┘
439  by { assume c, rintros ⟨f, hf⟩, simpa using integrable.smul _ }
id                                               └─────────────┘
src       └──────┘  └─────────────┘  └──────────┘└─────────────┘└─┘
typ       └──────┘  └─────────────┘  └──────────┘└─────────────┘└─┘
doc       └──────┘  └─────────────┘  └──────────┘               └─┘
txt       └──────┘  └─────────────┘  └──────────┘               └─┘
par       └──────┘  └─────────────┘  └──────────┘               └─┘
pid       └──────┘         └──────┘       └────┘               └┘
st     └─────────┘└───────────────┘└──────────────────────────────┘└┘
440  
441  end normed_space
442  
443  end ae_eq_fun
444  
445  section
446  variables (α β)
447  
448  /-- The space of equivalence classes of integrable (and measurable) functions, where two integrable
449      functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure
450      `0`. -/
451  def l1 : Type (max u v) := subtype (@ae_eq_fun.integrable α _ β _ _)
id                              └─────┘   └──────────────────┘    
src                             └─────┘   └──────────────────┘
typ                             └─────┘   └──────────────────┘    
doc                                       └──────────────────┘
452  
453  infixr ` →₁ `:25 := l1
id                       └┘
src                      └┘
typ                      └┘
doc                      └┘
454  
455  end
456  
457  namespace l1
458  open ae_eq_fun
459  local attribute [instance] ae_eq_fun.is_add_subgroup
id                              └───────────────────────┘
src                             └───────────────────────┘
typ                             └───────────────────────┘
460  
461  instance : has_coe (α →₁ β) (α →ₘ β) := ⟨subtype.val⟩
id              └─────┘   └┘     └┘       └─────────┘
src             └─────┘    └┘       └┘        └─────────┘
typ             └─────┘   └┘     └┘       └─────────┘
doc                        └┘       └┘
462  
463  protected lemma eq {f g : α →₁ β} : (f : α →ₘ β) = (g : α →ₘ β) → f = g := subtype.eq
id                              └┘          └┘         └┘           └────────┘
src                              └┘             └┘            └┘              └────────┘
typ                             └┘          └┘         └┘           └────────┘
doc                              └┘             └┘             └┘
464  @[elim_cast] protected lemma eq_iff {f g : α →₁ β} : (f : α →ₘ β) = (g : α →ₘ β) ↔ f = g :=
id                                               └┘          └┘         └┘      
src                                               └┘             └┘            └┘       
typ                                              └┘          └┘         └┘      
doc    └───────┘                                  └┘             └┘             └┘
465  iff.intro (l1.eq) (congr_arg coe)
id   └───────┘  └───┘   └───────┘ └─┘
src  └───────┘  └───┘   └───────┘ └─┘
typ  └───────┘  └───┘   └───────┘ └─┘
466  
467  /- TODO : order structure of l1-/
468  
469  /-- `L¹` space forms a `emetric_space`, with the emetric being inherited from almost everywhere
470    functions, i.e., `edist f g = ∫⁻ a, edist (f a) (g a)`. -/
471  instance : emetric_space (α →₁ β) := subtype.emetric_space
id              └───────────┘   └┘      └───────────────────┘
src             └───────────┘    └┘       └───────────────────┘
typ             └───────────┘   └┘      └───────────────────┘
doc             └───────────┘    └┘       └───────────────────┘
472  
473  /-- `L¹` space forms a `metric_space`, with the metric being inherited from almost everywhere
474    functions, i.e., `edist f g = ennreal.to_real (∫⁻ a, edist (f a) (g a))`. -/
475  instance : metric_space (α →₁ β) := metric_space_emetric_ball 0 ⊤
id              └──────────┘   └┘      └───────────────────────┘   
src             └──────────┘    └┘       └───────────────────────┘   
typ             └──────────┘   └┘      └───────────────────────┘   
doc             └──────────┘    └┘       └───────────────────────┘
476  instance : add_comm_group (α →₁ β) := subtype.add_comm_group
id              └────────────┘   └┘      └────────────────────┘
src             └────────────┘    └┘       └────────────────────┘
typ             └────────────┘   └┘      └────────────────────┘
doc                               └┘
477  
478  instance : inhabited (α →₁ β) := ⟨0⟩
id              └───────┘   └┘ 
src             └───────┘    └┘
typ             └───────┘   └┘ 
doc                          └┘
479  
480  @[simp, elim_cast] lemma coe_zero : ((0 : α →₁ β) : α →ₘ β) = 0 := rfl
id                                              └┘      └┘         └─┘
src                                              └┘        └┘          └─┘
typ                                             └┘      └┘         └─┘
doc    └──┘  └───────┘                           └┘        └┘
481  @[simp, move_cast] lemma coe_add (f g : α →₁ β) : ((f + g : α →₁ β) : α →ₘ β) = f + g := rfl
id                                            └┘             └┘      └┘          └─┘
src                                            └┘                 └┘        └┘             └─┘
typ                                           └┘             └┘      └┘          └─┘
doc    └──┘  └───────┘                         └┘                  └┘        └┘
482  @[simp, move_cast] lemma coe_neg (f : α →₁ β) : ((-f : α →₁ β) : α →ₘ β) = -f := rfl
id                                          └┘           └┘      └┘        └─┘
src                                          └┘              └┘        └┘          └─┘
typ                                         └┘           └┘      └┘        └─┘
doc    └──┘  └───────┘                       └┘               └┘        └┘
483  @[simp, move_cast] lemma coe_sub (f g : α →₁ β) : ((f - g : α →₁ β) : α →ₘ β) = f - g := rfl
id                                            └┘             └┘      └┘          └─┘
src                                            └┘                 └┘        └┘             └─┘
typ                                           └┘             └┘      └┘          └─┘
doc    └──┘  └───────┘                         └┘                  └┘        └┘
484  @[simp] lemma edist_eq (f g : α →₁ β) : edist f g = edist (f : α →ₘ β) (g : α →ₘ β) := rfl
id                                  └┘     └───┘    └───┘      └┘        └┘      └─┘
src                                  └┘      └───┘      └───┘        └┘           └┘       └─┘
typ                                 └┘     └───┘    └───┘      └┘        └┘      └─┘
doc    └──┘                          └┘                               └┘           └┘
485  
486  lemma dist_eq (f g : α →₁ β) : dist f g = ennreal.to_real (edist (f : α →ₘ β) (g : α →ₘ β)) := rfl
id                         └┘     └──┘    └─────────────┘  └───┘      └┘        └┘       └─┘
src                         └┘      └──┘      └─────────────┘  └───┘        └┘           └┘        └─┘
typ                        └┘     └──┘    └─────────────┘  └───┘      └┘        └┘       └─┘
doc                         └┘                 └─────────────┘               └┘           └┘
487  
488  /-- The norm on `L¹` space is defined to be `∥f∥ = ∫⁻ a, edist (f a) 0`. -/
489  instance : has_norm (α →₁ β) := ⟨λ f, dist f 0⟩
id              └──────┘   └┘           └──┘ 
src             └──────┘    └┘             └──┘
typ             └──────┘   └┘           └──┘ 
doc             └──────┘    └┘
490  
491  lemma norm_eq (f : α →₁ β) : ∥f∥ = ennreal.to_real (edist (f : α →ₘ β) 0) := rfl
id                       └┘       └─────────────┘  └───┘      └┘         └─┘
src                       └┘         └─────────────┘  └───┘        └┘          └─┘
typ                      └┘       └─────────────┘  └───┘      └┘         └─┘
doc                       └┘            └─────────────┘               └┘
492  
493  instance : normed_group (α →₁ β) := normed_group.of_add_dist (λ x, rfl) $ by
id              └──────────┘   └┘      └──────────────────────┘      └─┘
src             └──────────┘    └┘       └──────────────────────┘       └─┘
typ             └──────────┘   └┘      └──────────────────────┘      └─┘
doc             └──────────┘    └┘       └──────────────────────┘
st                                                                               
494  { intros, simp only [dist_eq, coe_add], rw edist_eq_add_add }
id                        └─────┘  └─────┘      └──────────────┘
src    └────┘  └─────────┘└─────┘└┘└─────┘  └─┘└──────────────┘
typ    └────┘  └─────────┘└─────┘└┘└─────┘  └─┘└──────────────┘
doc    └────┘  └─────────┘       └┘         └─┘                
txt    └────┘  └─────────┘       └┘         └─┘                
par    └────┘  └─────────┘       └┘         └─┘                
pid                └──┘└┘       └┘                           
st   ───────┘└────────────────────────────┘└────────────────────┘└┘
495  
496  section normed_space
497  
498  variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id                          └──────────┘     └──────────┘
src                         └──────────┘     └──────────┘
typ                         └──────────┘     └──────────┘
doc                         └──────────┘     └──────────┘
499  
500  instance : has_scalar 𝕜 (α →₁ β) := ⟨λ x f, ⟨x • (f : α →ₘ β), ae_eq_fun.integrable.smul f.2⟩⟩
id              └────────┘    └┘                    └┘    └───────────────────────┘ 
src             └────────┘      └┘                          └┘     └───────────────────────┘  
typ             └────────┘    └┘                    └┘    └───────────────────────┘ 
doc             └────────┘      └┘                           └┘
501  
502  @[simp, move_cast] lemma coe_smul (c : 𝕜) (f : α →₁ β) :
id                                                  └┘ 
src                                                   └┘
typ                                                 └┘ 
doc    └──┘  └───────┘                                └┘
503    ((c • f : α →₁ β) : α →ₘ β) = c • (f : α →ₘ β) := rfl
id             └┘      └┘           └┘      └─┘
src               └┘        └┘               └┘       └─┘
typ            └┘      └┘           └┘      └─┘
doc                └┘        └┘                 └┘
504  
505  instance : semimodule 𝕜 (α →₁ β) :=
id              └────────┘    └┘ 
src             └────────┘      └┘
typ             └────────┘    └┘ 
doc             └────────┘      └┘
506  { one_smul  := λf, l1.eq (by { simp only [coe_smul], exact one_smul _ _ }),
id                     └───┘                  └──────┘         └──────┘
src                     └───┘       └─────────┘└──────┘  └────┘└──────┘└───┘
typ                    └───┘       └─────────┘└──────┘  └────┘└──────┘└───┘
doc                                 └─────────┘          └────┘        └───┘
txt                                 └─────────┘          └────┘        └───┘
par                                 └─────────┘          └────┘        └───┘
pid                                     └──┘└┘                       └──┘
st                               └─────────────────────┘└───────────────────┘└┘
507    mul_smul  := λx y f, l1.eq (by { simp only [coe_smul], exact mul_smul _ _ _ }),
id                       └───┘                  └──────┘         └──────┘
src                         └───┘       └─────────┘└──────┘  └────┘└──────┘└─────┘
typ                      └───┘       └─────────┘└──────┘  └────┘└──────┘└─────┘
doc                                     └─────────┘          └────┘        └─────┘
txt                                     └─────────┘          └────┘        └─────┘
par                                     └─────────┘          └────┘        └─────┘
pid                                         └──┘└┘                       └────┘
st                                   └─────────────────────┘└─────────────────────┘└┘
508    smul_add  := λx f g, l1.eq (by { simp only [coe_smul, coe_add], exact smul_add _ _ _ }),
id                       └───┘                  └──────┘  └─────┘         └──────┘
src                         └───┘       └─────────┘└──────┘└┘└─────┘  └────┘└──────┘└─────┘
typ                      └───┘       └─────────┘└──────┘└┘└─────┘  └────┘└──────┘└─────┘
doc                                     └─────────┘        └┘         └────┘        └─────┘
txt                                     └─────────┘        └┘         └────┘        └─────┘
par                                     └─────────┘        └┘         └────┘        └─────┘
pid                                         └──┘└┘        └┘                      └────┘
st                                   └──────────────────────────────┘└─────────────────────┘└┘
509    smul_zero := λx, l1.eq (by { simp only [coe_zero, coe_smul], exact smul_zero _ }),
id                     └───┘                  └──────┘  └──────┘         └───────┘
src                     └───┘       └─────────┘└──────┘└┘└──────┘  └────┘└───────┘└─┘
typ                    └───┘       └─────────┘└──────┘└┘└──────┘  └────┘└───────┘└─┘
doc                                 └─────────┘        └┘          └────┘         └─┘
txt                                 └─────────┘        └┘          └────┘         └─┘
par                                 └─────────┘        └┘          └────┘         └─┘
pid                                     └──┘└┘        └┘                        └┘
st                               └───────────────────────────────┘└──────────────────┘└┘
510    add_smul  := λx y f, l1.eq (by { simp only [coe_smul], exact add_smul _ _ _ }),
id                       └───┘                  └──────┘         └──────┘
src                         └───┘       └─────────┘└──────┘  └────┘└──────┘└─────┘
typ                      └───┘       └─────────┘└──────┘  └────┘└──────┘└─────┘
doc                                     └─────────┘          └────┘        └─────┘
txt                                     └─────────┘          └────┘        └─────┘
par                                     └─────────┘          └────┘        └─────┘
pid                                         └──┘└┘                       └────┘
st                                   └─────────────────────┘└─────────────────────┘└┘
511    zero_smul := λf, l1.eq (by { simp only [coe_smul], exact zero_smul _ _ }) }
id                     └───┘                  └──────┘         └───────┘
src                     └───┘       └─────────┘└──────┘  └────┘└───────┘└───┘
typ                    └───┘       └─────────┘└──────┘  └────┘└───────┘└───┘
doc                                 └─────────┘          └────┘         └───┘
txt                                 └─────────┘          └────┘         └───┘
par                                 └─────────┘          └────┘         └───┘
pid                                     └──┘└┘                        └──┘
st                               └─────────────────────┘└────────────────────┘└┘
512  
513  instance : module 𝕜 (α →₁ β) := { .. l1.semimodule }
id              └────┘    └┘           └───────────┘
src             └────┘      └┘            └───────────┘
typ             └────┘    └┘           └───────────┘
doc             └────┘      └┘
514  
515  instance : vector_space 𝕜 (α →₁ β) := { .. l1.semimodule }
id              └──────────┘    └┘           └───────────┘
src             └──────────┘      └┘            └───────────┘
typ             └──────────┘    └┘           └───────────┘
doc             └──────────┘      └┘
516  
517  instance : normed_space 𝕜 (α →₁ β) :=
id              └──────────┘    └┘ 
src             └──────────┘      └┘
typ             └──────────┘    └┘ 
doc             └──────────┘      └┘
518  ⟨ begin
st     └─────
519      rintros x ⟨f, hf⟩,
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
txt      └───────────────┘
par      └───────────────┘
pid             └────────┘
st   ────────────────────┘└─
520      show ennreal.to_real (edist (x • f) 0) = ∥x∥ * ennreal.to_real (edist f 0),
id                                                └─────────────┘  └───┘ 
src      └───┘                        └───┘ └─────────────┘ └───┘ └─┘
typ      └───┘                        └───┘└─────────────┘ └───┘└─┘
doc      └───┘                         └───┘     └─────────────┘       └─┘
txt      └───┘                         └───┘                           └─┘
par      └───┘                         └───┘                           └─┘
pid      └───┘                         └───┘                           └─┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
521      rw [edist_smul, to_real_of_real_mul],
id           └────────┘  └─────────────────┘
src      └──┘└────────┘└┘└─────────────────┘
typ      └──┘└────────┘└┘└─────────────────┘
doc      └──┘          └┘                   
txt      └──┘          └┘                   
par      └──┘          └┘                   
pid        └┘          └┘                   
st   ─────────────────┘└───────────────────┘└──
522      exact norm_nonneg _
id             └─────────┘
src      └────┘└─────────┘└──
typ      └────┘└─────────┘└──
doc      └────┘           └──
txt      └────┘           └──
par      └────┘           └──
pid                      └┘
st   ────────────────────────
523    end ⟩
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
524  
525  end normed_space
526  
527  section of_fun
528  
529  /-- Construct the equivalence class `[f]` of a measurable and integrable function `f`. -/
530  def of_fun (f : α → β) (hfm : measurable f) (hfi : integrable f) : (α →₁ β) :=
id                               └────────┘          └────────┘       └┘ 
src                                └────────┘           └────────┘         └┘
typ                              └────────┘          └────────┘       └┘ 
doc                                └────────┘           └────────┘         └┘
531  ⟨mk f hfm, by { rw integrable_mk, exact hfi }⟩
id    └┘  └─┘          └───────────┘        └─┘
src   └┘             └─┘└───────────┘  └────┘   
typ   └┘  └─┘       └─┘└───────────┘  └────┘└─┘
doc   └┘             └─┘               └────┘   
txt                  └─┘               └────┘   
par                  └─┘               └────┘   
pid                                           
st                └─────────────────┘└──────────┘└┘
532  
533  lemma of_fun_eq_mk (f : α → β) (hfm hfi) : (of_fun f hfm hfi : α →ₘ β) = mk f hfm := rfl
id                                             └────┘  └─┘ └─┘    └┘    └┘  └─┘    └─┘
src                                              └────┘               └┘     └┘          └─┘
typ                                            └────┘  └─┘ └─┘    └┘    └┘  └─┘    └─┘
doc                                              └────┘               └┘      └┘
534  
535  lemma of_fun_eq_of_fun (f g : α → β) (hfm hfi hgm hgi) :
id                                    
typ                                   
536    of_fun f hfm hfi = of_fun g hgm hgi ↔ ∀ₘ a, f a = g a :=
id     └────┘  └─┘ └─┘  └────┘  └─┘ └─┘  └┘      
src    └────┘            └────┘            └┘       
typ    └────┘  └─┘ └─┘  └────┘  └─┘ └─┘  └┘      
doc    └────┘             └────┘             └┘  
537  by { rw ← l1.eq_iff, simp only [of_fun_eq_mk, mk_eq_mk] }
id             └───────┘             └──────────┘  └──────┘
src       └───┘└───────┘  └─────────┘└──────────┘└┘└──────┘└┘
typ       └───┘└───────┘  └─────────┘└──────────┘└┘└──────┘└┘
doc       └───┘           └─────────┘            └┘        └┘
txt       └───┘           └─────────┘            └┘        └┘
par       └───┘           └─────────┘            └┘        └┘
pid         └─┘               └──┘└┘            └┘        
st     └───────────────┘└───────────────────────────────────┘└┘
538  
539  lemma of_fun_zero :
540    of_fun (λa:α, (0:β)) (@measurable_const _ _ _ _ (0:β)) (integrable_zero α β) = 0 := rfl
id     └────┘               └──────────────┘                └─────────────┘          └─┘
src    └────┘                 └──────────────┘                 └─────────────┘            └─┘
typ    └────┘               └──────────────┘                └─────────────┘          └─┘
doc    └────┘
541  
542  lemma of_fun_add (f g : α → β) (hfm hfi hgm hgi) :
id                              
typ                             
543    of_fun (λa, f a + g a) (measurable.add hfm hgm) (integrable.add hfm hfi hgm hgi)
id     └────┘            └────────────┘ └─┘ └─┘   └────────────┘ └─┘ └─┘ └─┘ └─┘
src    └────┘                 └────────────┘           └────────────┘
typ    └────┘            └────────────┘ └─┘ └─┘   └────────────┘ └─┘ └─┘ └─┘ └─┘
doc    └────┘
544      = of_fun f hfm hfi + of_fun g hgm hgi :=
id        └────┘  └─┘ └─┘  └────┘  └─┘ └─┘
src       └────┘            └────┘
typ       └────┘  └─┘ └─┘  └────┘  └─┘ └─┘
doc        └────┘             └────┘
545  rfl
id   └─┘
src  └─┘
typ  └─┘
546  
547  lemma of_fun_neg (f : α → β) (hfm hfi) :
id                            
typ                           
548    of_fun (λa, - f a) (measurable.neg hfm) (integrable.neg hfi) = - of_fun f hfm hfi := rfl
id     └────┘          └────────────┘ └─┘   └────────────┘ └─┘    └────┘  └─┘ └─┘    └─┘
src    └────┘             └────────────┘       └────────────┘        └────┘              └─┘
typ    └────┘          └────────────┘ └─┘   └────────────┘ └─┘    └────┘  └─┘ └─┘    └─┘
doc    └────┘                                                           └────┘
549  
550  lemma of_fun_sub (f g : α → β) (hfm hfi hgm hgi) :
id                              
typ                             
551    of_fun (λa, f a - g a) (measurable.sub hfm hgm) (integrable.sub hfm hfi hgm hgi)
id     └────┘            └────────────┘ └─┘ └─┘   └────────────┘ └─┘ └─┘ └─┘ └─┘
src    └────┘                 └────────────┘           └────────────┘
typ    └────┘            └────────────┘ └─┘ └─┘   └────────────┘ └─┘ └─┘ └─┘ └─┘
doc    └────┘
552      = of_fun f hfm hfi - of_fun g hgm hgi :=
id        └────┘  └─┘ └─┘  └────┘  └─┘ └─┘
src       └────┘            └────┘
typ       └────┘  └─┘ └─┘  └────┘  └─┘ └─┘
doc        └────┘             └────┘
553  rfl
id   └─┘
src  └─┘
typ  └─┘
554  
555  lemma norm_of_fun (f : α → β) (hfm hfi) : ∥of_fun f hfm hfi∥ = ennreal.to_real (∫⁻ a, edist (f a) 0) :=
id                                           └────┘  └─┘ └─┘  └─────────────┘  └┘  └───┘   
src                                            └────┘            └─────────────┘  └┘   └───┘
typ                                          └────┘  └─┘ └─┘  └─────────────┘  └┘  └───┘   
doc                                             └────┘              └─────────────┘  └┘  
556  rfl
id   └─┘
src  └─┘
typ  └─┘
557  
558  lemma norm_of_fun_eq_lintegral_norm (f : α → β) (hfm hfi) :
id                                               
typ                                              
559    ∥of_fun f hfm hfi∥ = ennreal.to_real (∫⁻ a, ennreal.of_real ∥f a∥) :=
id     └────┘  └─┘ └─┘  └─────────────┘  └┘  └─────────────┘  
src    └────┘            └─────────────┘  └┘   └─────────────┘    
typ    └────┘  └─┘ └─┘  └─────────────┘  └┘  └─────────────┘  
doc     └────┘              └─────────────┘  └┘   └─────────────┘
560  by { rw [norm_of_fun, lintegral_norm_eq_lintegral_edist] }
id            └─────────┘  └───────────────────────────────┘
src       └──┘└─────────┘└┘└───────────────────────────────┘└┘
typ       └──┘└─────────┘└┘└───────────────────────────────┘└┘
doc       └──┘           └┘                                 └┘
txt       └──┘           └┘                                 └┘
par       └──┘           └┘                                 └┘
pid         └┘           └┘                                 
st     └────────────────┘└─────────────────────────────────┘└┘
561  
562  variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id                          └──────────┘     └──────────┘
src                         └──────────┘     └──────────┘
typ                         └──────────┘     └──────────┘
doc                         └──────────┘     └──────────┘
563  
564  lemma of_fun_smul (f : α → β) (hfm hfi) (k : 𝕜) :
id                                              
typ                                             
565    of_fun (λa, k • f a) (measurable.smul _ hfm) (integrable.smul _ hfi) = k • of_fun f hfm hfi := rfl
id     └────┘           └─────────────┘   └─┘   └─────────────┘   └─┘     └────┘  └─┘ └─┘    └─┘
src    └────┘               └─────────────┘         └─────────────┘            └────┘              └─┘
typ    └────┘           └─────────────┘   └─┘   └─────────────┘   └─┘     └────┘  └─┘ └─┘    └─┘
doc    └────┘                                                                     └────┘
566  
567  end of_fun
568  
569  section to_fun
570  
571  /-- Find a representative of a `L¹` function [f] -/
572  @[reducible]
doc    └───────┘
573  protected def to_fun (f : α →₁ β) : α → β := (f : α →ₘ β).to_fun
id                              └┘                 └┘  └────┘
src                              └┘                      └┘   └────┘
typ                             └┘                 └┘  └────┘
doc                              └┘                      └┘   └────┘
574  
575  protected lemma measurable (f : α →₁ β) : measurable f.to_fun := f.1.measurable
id                                    └┘     └────────┘ └─────┘     └────────┘
src                                    └┘      └────────┘  └─────┘      └────────┘
typ                                   └┘     └────────┘ └─────┘     └────────┘
doc                                    └┘      └────────┘  └─────┘
576  
577  protected lemma integrable (f : α →₁ β) : integrable f.to_fun :=
id                                    └┘     └────────┘ └─────┘
src                                    └┘      └────────┘  └─────┘
typ                                   └┘     └────────┘ └─────┘
doc                                    └┘      └────────┘  └─────┘
578  by { rw [l1.to_fun, ← integrable_to_fun], exact f.2 }
id            └───────┘    └───────────────┘         
src       └──┘└───────┘└──┘└───────────────┘  └────┘ └─┘
typ       └──┘└───────┘└──┘└───────────────┘  └────┘└─┘
doc       └──┘└───────┘└──┘                   └────┘ └─┘
txt       └──┘         └──┘                   └────┘ └─┘
par       └──┘         └──┘                   └────┘ └─┘
pid         └┘         └──┘                         └─┘
st     └──────────────┘└───────────────────┘└───────────┘└┘
579  
580  lemma of_fun_to_fun (f : α →₁ β) : of_fun (f.to_fun) f.measurable f.integrable = f :=
id                             └┘     └────┘  └─────┘  └─────────┘ └─────────┘  
src                             └┘      └────┘   └─────┘   └─────────┘  └─────────┘ 
typ                            └┘     └────┘  └─────┘  └─────────┘ └─────────┘  
doc                             └┘      └────┘   └─────┘
581  begin
st   └─────
582    rcases f with ⟨f, hfi⟩,
id            
src    └─────┘ └────────────┘
typ    └─────┘└────────────┘
doc    └─────┘ └────────────┘
txt    └─────┘ └────────────┘
par    └─────┘ └────────────┘
pid           └────────────┘
st   ───────────────────────┘└─
583    rw [of_fun, subtype.mk_eq_mk],
id         └────┘  └──────────────┘
src    └──┘└────┘└┘└──────────────┘
typ    └──┘└────┘└┘└──────────────┘
doc    └──┘└────┘└┘                
txt    └──┘      └┘                
par    └──┘      └┘                
pid      └┘      └┘                
st   ───────────┘└────────────────┘└──
584    exact (self_eq_mk f).symm
id            └────────┘ 
src    └────┘ └────────┘ └─────┘
typ    └────┘ └────────┘└─────┘
doc    └────┘            └─────┘
txt    └────┘            └─────┘
par    └────┘            └─────┘
pid                     └───┘└┘
st   ───────────────────────────┘
585  end
st   └─┘
586  
587  lemma mk_to_fun (f : α →₁ β) : mk (f.to_fun) f.measurable = f :=
id                         └┘     └┘  └─────┘  └─────────┘  
src                         └┘      └┘   └─────┘   └─────────┘ 
typ                        └┘     └┘  └─────┘  └─────────┘  
doc                         └┘      └┘   └─────┘
588  by { rw ← of_fun_eq_mk, rw l1.eq_iff, exact of_fun_to_fun f }
id             └──────────┘     └───────┘        └───────────┘ 
src       └───┘└──────────┘  └─┘└───────┘  └────┘└───────────┘ 
typ       └───┘└──────────┘  └─┘└───────┘  └────┘└───────────┘
doc       └───┘              └─┘           └────┘              
txt       └───┘              └─┘           └────┘              
par       └───┘              └─┘           └────┘              
pid         └─┘                                              
st     └──────────────────┘└────────────┘└──────────────────────┘└┘
589  
590  lemma to_fun_of_fun (f : α → β) (hfm hfi) : ∀ₘ a, (of_fun f hfm hfi).to_fun a = f a :=
id                                             └┘   └────┘  └─┘ └─┘ └────┘     
src                                              └┘    └────┘           └────┘    
typ                                            └┘   └────┘  └─┘ └─┘ └────┘     
doc                                              └┘    └────┘           └────┘
591  begin
st   └─────
592    filter_upwards [all_ae_mk_to_fun f hfm],
id                     └──────────────┘  └─┘
src    └──────────────┘└──────────────┘    
typ    └──────────────┘└──────────────┘└─┘
doc    └──────────────┘                    
txt    └──────────────┘                    
par    └──────────────┘                    
pid                  └┘                    
st   ────────────────────────────────────────┘└─
593    assume a,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
594    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
595    assume h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
596    rw ← h,
id          
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ───────┘└─
597    refl
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
598  end
st   └─┘
599  
600  variables (α β)
601  lemma zero_to_fun : ∀ₘ a, (0 : α →₁ β).to_fun a = 0 := ae_eq_fun.zero_to_fun
id                       └┘        └┘  └────┘         └───────────────────┘
src                      └┘          └┘   └────┘          └───────────────────┘
typ                      └┘        └┘  └────┘         └───────────────────┘
doc                      └┘          └┘   └────┘
602  variables {α β}
603  
604  lemma add_to_fun (f g : α →₁ β) : ∀ₘ a, (f + g).to_fun a = f.to_fun a + g.to_fun a :=
id                            └┘     └┘      └────┘    └─────┘   └─────┘ 
src                            └┘      └┘         └────┘      └─────┘     └─────┘
typ                           └┘     └┘      └────┘    └─────┘   └─────┘ 
doc                            └┘      └┘          └────┘       └─────┘      └─────┘
605  ae_eq_fun.add_to_fun _ _
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
606  
607  lemma neg_to_fun (f : α →₁ β) : ∀ₘ a, (-f).to_fun a = -f.to_fun a := ae_eq_fun.neg_to_fun _
id                          └┘     └┘    └────┘    └─────┘     └──────────────────┘
src                          └┘      └┘      └────┘      └─────┘      └──────────────────┘
typ                         └┘     └┘    └────┘    └─────┘     └──────────────────┘
doc                          └┘      └┘       └────┘        └─────┘
608  
609  lemma sub_to_fun (f g : α →₁ β) : ∀ₘ a, (f - g).to_fun a = f.to_fun a - g.to_fun a :=
id                            └┘     └┘      └────┘    └─────┘   └─────┘ 
src                            └┘      └┘         └────┘      └─────┘     └─────┘
typ                           └┘     └┘      └────┘    └─────┘   └─────┘ 
doc                            └┘      └┘          └────┘       └─────┘      └─────┘
610  ae_eq_fun.sub_to_fun _ _
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
611  
612  lemma dist_to_fun (f g : α →₁ β) : dist f g = ennreal.to_real (∫⁻ x, edist (f.to_fun x) (g.to_fun x)) :=
id                             └┘     └──┘    └─────────────┘  └┘  └───┘  └─────┘    └─────┘ 
src                             └┘      └──┘      └─────────────┘  └┘   └───┘   └─────┘      └─────┘
typ                            └┘     └──┘    └─────────────┘  └┘  └───┘  └─────┘    └─────┘ 
doc                             └┘                 └─────────────┘  └┘           └─────┘      └─────┘
613  by { simp only [dist_eq, edist_to_fun] }
id                   └─────┘  └──────────┘
src       └─────────┘└─────┘└┘└──────────┘└┘
typ       └─────────┘└─────┘└┘└──────────┘└┘
doc       └─────────┘       └┘            └┘
txt       └─────────┘       └┘            └┘
par       └─────────┘       └┘            └┘
pid           └──┘└┘       └┘            
st     └───────────────────────────────────┘└┘
614  
615  lemma norm_eq_nnnorm_to_fun (f : α →₁ β) : ∥f∥ = ennreal.to_real (∫⁻ a, nnnorm (f.to_fun a)) :=
id                                     └┘       └─────────────┘  └┘  └────┘  └─────┘ 
src                                     └┘         └─────────────┘  └┘   └────┘   └─────┘
typ                                    └┘       └─────────────┘  └┘  └────┘  └─────┘ 
doc                                     └┘            └─────────────┘  └┘   └────┘   └─────┘
616  by { rw [lintegral_nnnorm_eq_lintegral_edist, ← edist_zero_to_fun], refl }
id            └─────────────────────────────────┘    └───────────────┘
src       └──┘└─────────────────────────────────┘└──┘└───────────────┘  └───┘
typ       └──┘└─────────────────────────────────┘└──┘└───────────────┘  └───┘
doc       └──┘                                   └──┘                   └───┘
txt       └──┘                                   └──┘                   └───┘
par       └──┘                                   └──┘                   └───┘
pid         └┘                                   └──┘                       
st     └────────────────────────────────────────┘└───────────────────┘└──────┘└┘
617  
618  lemma norm_eq_norm_to_fun (f : α →₁ β) : ∥f∥ = ennreal.to_real (∫⁻ a, ennreal.of_real ∥f.to_fun a∥) :=
id                                   └┘       └─────────────┘  └┘  └─────────────┘ └─────┘ 
src                                   └┘         └─────────────┘  └┘   └─────────────┘  └─────┘  
typ                                  └┘       └─────────────┘  └┘  └─────────────┘ └─────┘ 
doc                                   └┘            └─────────────┘  └┘   └─────────────┘   └─────┘
619  by { rw norm_eq_nnnorm_to_fun, congr, funext, rw of_real_norm_eq_coe_nnnorm }
id           └───────────────────┘                    └────────────────────────┘
src       └─┘└───────────────────┘  └───┘  └────┘  └─┘└────────────────────────┘
typ       └─┘└───────────────────┘  └───┘  └────┘  └─┘└────────────────────────┘
doc       └─┘                              └────┘  └─┘                          
txt       └─┘                       └───┘  └────┘  └─┘                          
par       └─┘                       └───┘  └────┘  └─┘                          
pid                                                                           
st     └─────────────────────────┘└─────┘└──────┘└──────────────────────────────┘└┘
620  
621  lemma lintegral_edist_to_fun_lt_top (f g : α →₁ β) : (∫⁻ a, edist (f.to_fun a) (g.to_fun a)) < ⊤ :=
id                                               └┘      └┘  └───┘  └─────┘    └─────┘     
src                                               └┘       └┘   └───┘   └─────┘      └─────┘      
typ                                              └┘      └┘  └───┘  └─────┘    └─────┘     
doc                                               └┘       └┘           └─────┘      └─────┘
622  begin
st   └─────
623    apply lintegral_edist_lt_top,
id           └────────────────────┘
src    └────┘└────────────────────┘
typ    └────┘└────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────────┘└─
624    exact f.measurable, exact f.integrable, exact g.measurable, exact g.integrable
id           └──────────┘        └──────────┘        └──────────┘        └──────────┘
src    └────┘└──────────┘  └────┘└──────────┘  └────┘└──────────┘  └────┘└──────────┘
typ    └────┘└──────────┘  └────┘└──────────┘  └────┘└──────────┘  └────┘└──────────┘
doc    └────┘              └────┘              └────┘              └────┘            
txt    └────┘              └────┘              └────┘              └────┘            
par    └────┘              └────┘              └────┘              └────┘            
pid                                                                              
st   ───────────────────┘└──────────────────┘└──────────────────┘└───────────────────┘
625  end
st   └─┘
626  
627  variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id                          └──────────┘     └──────────┘
src                         └──────────┘     └──────────┘
typ                         └──────────┘     └──────────┘
doc                         └──────────┘     └──────────┘
628  
629  lemma smul_to_fun (c : 𝕜) (f : α →₁ β) : ∀ₘ a, (c • f).to_fun a = c • f.to_fun a :=
id                                  └┘     └┘      └────┘      └─────┘ 
src                                   └┘      └┘         └────┘         └─────┘
typ                                 └┘     └┘      └────┘      └─────┘ 
doc                                   └┘      └┘          └────┘           └─────┘
630  ae_eq_fun.smul_to_fun _ _
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
631  
632  end to_fun
633  
634  section pos_part
635  
636  /-- Positive part of a function in `L¹` space. -/
637  def pos_part (f : α →₁ ℝ) : α →₁ ℝ :=
id                      └┘      └┘ 
src                      └┘       └┘ 
typ                     └┘      └┘ 
doc                      └┘        └┘
638  ⟨ ae_eq_fun.pos_part f,
id     └────────────────┘ 
src    └────────────────┘
typ    └────────────────┘ 
doc    └────────────────┘
639    begin
st     └─────
640      rw [ae_eq_fun.integrable_to_fun, integrable_congr_ae (pos_part_to_fun _)],
id           └─────────────────────────┘  └─────────────────┘  └─────────────┘
src      └──┘└─────────────────────────┘└┘└─────────────────┘ └─────────────┘└──┘
typ      └──┘└─────────────────────────┘└┘└─────────────────┘ └─────────────┘└──┘
doc      └──┘                           └┘                                   └──┘
txt      └──┘                           └┘                                   └──┘
par      └──┘                           └┘                                   └──┘
pid        └┘                           └┘                                   └──┘
st   ──────────────────────────────────┘└───────────────────────────────────────┘└──
641      exact integrable.max_zero f.integrable
id             └─────────────────┘ └──────────┘
src      └────┘└─────────────────┘└──────────┘
typ      └────┘└─────────────────┘└──────────┘
doc      └────┘                               
txt      └────┘                               
par      └────┘                               
pid                                          
st   ───────────────────────────────────────────
642    end ⟩
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
643  
644  /-- Negative part of a function in `L¹` space. -/
645  def neg_part (f : α →₁ ℝ) : α →₁ ℝ := pos_part (-f)
id                      └┘      └┘     └──────┘  
src                      └┘       └┘     └──────┘  
typ                     └┘      └┘     └──────┘  
doc                      └┘        └┘      └──────┘
646  
647  @[move_cast] lemma coe_pos_part (f : α →₁ ℝ) : (f.pos_part : α →ₘ ℝ) = (f : α →ₘ ℝ).pos_part := rfl
id                                         └┘      └───────┘    └┘         └┘  └──────┘     └─┘
src                                         └┘       └───────┘     └┘           └┘  └──────┘     └─┘
typ                                        └┘      └───────┘    └┘         └┘  └──────┘     └─┘
doc    └───────┘                            └┘        └───────┘     └┘             └┘   └──────┘
648  
649  lemma pos_part_to_fun (f : α →₁ ℝ) : ∀ₘ a, (pos_part f).to_fun a = max (f.to_fun a) 0 :=
id                               └┘     └┘   └──────┘  └────┘    └─┘  └─────┘ 
src                               └┘     └┘    └──────┘   └────┘     └─┘   └─────┘
typ                              └┘     └┘   └──────┘  └────┘    └─┘  └─────┘ 
doc                               └┘      └┘    └──────┘   └────┘            └─────┘
650  ae_eq_fun.pos_part_to_fun _
id   └───────────────────────┘
src  └───────────────────────┘
typ  └───────────────────────┘
651  
652  lemma neg_part_to_fun_eq_max (f : α →₁ ℝ) : ∀ₘ a, (neg_part f).to_fun a = max (- f.to_fun a) 0 :=
id                                      └┘     └┘   └──────┘  └────┘    └─┘   └─────┘ 
src                                      └┘     └┘    └──────┘   └────┘     └─┘    └─────┘
typ                                     └┘     └┘   └──────┘  └────┘    └─┘   └─────┘ 
doc                                      └┘      └┘    └──────┘   └────┘              └─────┘
653  begin
st   └─────
654    rw neg_part,
id        └──────┘
src    └─┘└──────┘
typ    └─┘└──────┘
doc    └─┘└──────┘
txt    └─┘
par    └─┘
pid      
st   ────────────┘└─
655    filter_upwards [pos_part_to_fun (-f), neg_to_fun f],
id                     └─────────────┘     └────────┘ 
src    └──────────────┘└─────────────┘  └─┘└────────┘ 
typ    └──────────────┘└─────────────┘ └─┘└────────┘
doc    └──────────────┘                  └─┘           
txt    └──────────────┘                  └─┘           
par    └──────────────┘                  └─┘           
pid                  └┘                  └─┘           
st   ────────────────────────────────────────────────────┘└─
656    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
657    assume a h₁ h₂,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid    └────────────┘
st   ───────────────┘└─
658    rw [h₁, h₂]
id         └┘  └┘
src    └──┘  └┘  └┘
typ    └──┘└┘└┘└┘└┘
doc    └──┘  └┘  └┘
txt    └──┘  └┘  └┘
par    └──┘  └┘  └┘
pid      └┘  └┘  
st   ───────┘└──┘
659  end
st   └─┘
660  
661  lemma neg_part_to_fun_eq_min (f : α →₁ ℝ) : ∀ₘ a, (neg_part f).to_fun a = - min (f.to_fun a) 0 :=
id                                      └┘     └┘   └──────┘  └────┘     └─┘  └─────┘ 
src                                      └┘     └┘    └──────┘   └────┘      └─┘   └─────┘
typ                                     └┘     └┘   └──────┘  └────┘     └─┘  └─────┘ 
doc                                      └┘      └┘    └──────┘   └────┘              └─────┘
662  begin
st   └─────
663    filter_upwards [neg_part_to_fun_eq_max f],
id                     └────────────────────┘ 
src    └──────────────┘└────────────────────┘ 
typ    └──────────────┘└────────────────────┘
doc    └──────────────┘                       
txt    └──────────────┘                       
par    └──────────────┘                       
pid                  └┘                       
st   ──────────────────────────────────────────┘└─
664    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
665    assume a h,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid    └────────┘
st   ───────────┘└─
666    rw [h, min_eq_neg_max_neg_neg, _root_.neg_neg, neg_zero],
id           └────────────────────┘  └────────────┘  └──────┘
src    └──┘ └┘└────────────────────┘└┘└────────────┘└┘└──────┘
typ    └──┘└┘└────────────────────┘└┘└────────────┘└┘└──────┘
doc    └──┘ └┘                      └┘              └┘        
txt    └──┘ └┘                      └┘              └┘        
par    └──┘ └┘                      └┘              └┘        
pid      └┘ └┘                      └┘              └┘        
st   ──────┘└──────────────────────┘└──────────────┘└────────┘└──
667  end
st   ──┘
668  
669  lemma norm_le_norm_of_ae_le {f g : α →₁ β} (h : ∀ₘ a, ∥f.to_fun a∥ ≤ ∥g.to_fun a∥) : ∥f∥ ≤ ∥g∥ :=
id                                       └┘        └┘  └─────┘   └─────┘       
src                                       └┘         └┘    └─────┘     └─────┘          
typ                                      └┘        └┘  └─────┘   └─────┘       
doc                                       └┘         └┘     └─────┘        └─────┘
670  begin
st   └─────
671    simp only [l1.norm_eq_norm_to_fun],
id                └────────────────────┘
src    └─────────┘└────────────────────┘
typ    └─────────┘└────────────────────┘
doc    └─────────┘                      
txt    └─────────┘                      
par    └─────────┘                      
pid        └──┘└┘                      
st   ───────────────────────────────────┘└─
672    rw to_real_le_to_real,
id        └────────────────┘
src    └─┘└────────────────┘
typ    └─┘└────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────────┘└─
673    { apply lintegral_le_lintegral_ae,
id             └───────────────────────┘
src      └────┘└───────────────────────┘
typ      └────┘└───────────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└─────────────────────────────┘└─
674      filter_upwards [h],
src      └──────────────┘ 
typ      └──────────────┘ 
doc      └──────────────┘ 
txt      └──────────────┘ 
par      └──────────────┘ 
pid                    └┘ 
st   ─────────────────────┘└─
675      simp only [mem_set_of_eq],
id                  └───────────┘
src      └─────────┘└───────────┘
typ      └─────────┘└───────────┘
doc      └─────────┘             
txt      └─────────┘             
par      └─────────┘             
pid          └──┘└┘             
st   ────────────────────────────┘└─
676      assume a h,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid      └────────┘
st   ─────────────┘└─
677      exact of_real_le_of_real h },
id             └────────────────┘ 
src      └────┘└────────────────┘ 
typ      └────┘└────────────────┘
doc      └────┘                   
txt      └────┘                   
par      └────┘                   
pid                              
st   ──────────────────────────────┘└┘
678    { rw [← lt_top_iff_ne_top, ← integrable_iff_norm], exact f.integrable },
id             └───────────────┘    └─────────────────┘         └──────────┘
src      └────┘└───────────────┘└──┘└─────────────────┘  └────┘└──────────┘
typ      └────┘└───────────────┘└──┘└─────────────────┘  └────┘└──────────┘
doc      └────┘                 └──┘                     └────┘            
txt      └────┘                 └──┘                     └────┘            
par      └────┘                 └──┘                     └────┘            
pid        └──┘                 └──┘                                      
st   ───┘└─────────────────────┘└─────────────────────┘└────────────────────┘└┘
679    { rw [← lt_top_iff_ne_top, ← integrable_iff_norm], exact g.integrable }
id             └───────────────┘    └─────────────────┘         └──────────┘
src      └────┘└───────────────┘└──┘└─────────────────┘  └────┘└──────────┘
typ      └────┘└───────────────┘└──┘└─────────────────┘  └────┘└──────────┘
doc      └────┘                 └──┘                     └────┘            
txt      └────┘                 └──┘                     └────┘            
par      └────┘                 └──┘                     └────┘            
pid        └──┘                 └──┘                                      
st   ──────────────────────────┘└─────────────────────┘└────────────────────┘└─
680  end
st   ──┘
681  
682  lemma continuous_pos_part : continuous $ λf : α →₁ ℝ, pos_part f :=
id                               └────────┘         └┘   └──────┘ 
src                              └────────┘          └┘   └──────┘
typ                              └────────┘         └┘   └──────┘ 
doc                              └────────┘          └┘    └──────┘
683  begin
st   └─────
684    simp only [metric.continuous_iff],
id                └───────────────────┘
src    └─────────┘└───────────────────┘
typ    └─────────┘└───────────────────┘
doc    └─────────┘                     
txt    └─────────┘                     
par    └─────────┘                     
pid        └──┘└┘                     
st   ──────────────────────────────────┘└─
685    assume g ε hε,
src    └───────────┘
typ    └───────────┘
doc    └───────────┘
txt    └───────────┘
par    └───────────┘
pid    └───────────┘
st   ──────────────┘└─
686    use ε, use hε,
id               └┘
src    └──┘   └──┘
typ    └──┘  └──┘└┘
doc    └──┘   └──┘
txt    └──┘   └──┘
par    └──┘   └──┘
pid             
st   ──────┘└──────┘└─
687    simp only [dist_eq_norm],
id                └──────────┘
src    └─────────┘└──────────┘
typ    └─────────┘└──────────┘
doc    └─────────┘            
txt    └─────────┘            
par    └─────────┘            
pid        └──┘└┘            
st   ─────────────────────────┘└─
688    assume f hfg,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid    └──────────┘
st   ─────────────┘└─
689    refine lt_of_le_of_lt (norm_le_norm_of_ae_le _) hfg,
id            └────────────┘  └───────────────────┘    └─┘
src    └─────┘└────────────┘ └───────────────────┘└──┘
typ    └─────┘└────────────┘ └───────────────────┘└──┘└─┘
doc    └─────┘                                    └──┘
txt    └─────┘                                    └──┘
par    └─────┘                                    └──┘
pid                                              └──┘
st   ────────────────────────────────────────────────────┘└─
690    filter_upwards [l1.sub_to_fun f g, l1.sub_to_fun (pos_part f) (pos_part g),
id                     └───────────┘    └───────────┘              └──────┘ 
src    └──────────────┘└───────────┘  └┘└───────────┘          └┘ └──────┘ └──
typ    └──────────────┘└───────────┘└┘└───────────┘         └┘ └──────┘└──
doc    └──────────────┘               └┘                       └┘ └──────┘ └──
txt    └──────────────┘               └┘                       └┘          └──
par    └──────────────┘               └┘                       └┘          └──
pid                  └┘               └┘                       └┘          └──
st   ──────────────────────────────────────────────────────────────────────────────
691      pos_part_to_fun f, pos_part_to_fun g],
id       └─────────────┘   └─────────────┘ 
src  ───┘└─────────────┘ └┘└─────────────┘ 
typ  ───┘└─────────────┘└┘└─────────────┘
doc  ───┘                └┘                
txt  ───┘                └┘                
par  ───┘                └┘                
pid  ───┘                └┘                
st   ────────────────────────────────────────┘└─
692    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
693    assume a h₁ h₂ h₃ h₄,
src    └──────────────────┘
typ    └──────────────────┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid    └──────────────────┘
st   ─────────────────────┘└─
694    simp only [real.norm_eq_abs, h₁, h₂, h₃, h₄],
id                └──────────────┘  └┘  └┘  └┘  └┘
src    └─────────┘└──────────────┘└┘  └┘  └┘  └┘  
typ    └─────────┘└──────────────┘└┘└┘└┘└┘└┘└┘└┘└┘
doc    └─────────┘                └┘  └┘  └┘  └┘  
txt    └─────────┘                └┘  └┘  └┘  └┘  
par    └─────────┘                └┘  └┘  └┘  └┘  
pid        └──┘└┘                └┘  └┘  └┘  └┘  
st   ─────────────────────────────────────────────┘└─
695    exact abs_max_sub_max_le_abs _ _ _
id           └────────────────────┘
src    └────┘└────────────────────┘└─────┘
typ    └────┘└────────────────────┘└─────┘
doc    └────┘                      └─────┘
txt    └────┘                      └─────┘
par    └────┘                      └─────┘
pid                               └────┘
st   ────────────────────────────────────┘
696  end
st   └─┘
697  
698  lemma continuous_neg_part : continuous $ λf : α →₁ ℝ, neg_part f :=
id                               └────────┘         └┘   └──────┘ 
src                              └────────┘          └┘   └──────┘
typ                              └────────┘         └┘   └──────┘ 
doc                              └────────┘          └┘    └──────┘
699  have eq : (λf : α →₁ ℝ, neg_part f) = (λf : α →₁ ℝ, pos_part (-f)) := rfl,
id                    └┘   └──────┘           └┘   └──────┘        └─┘
src                    └┘   └──────┘             └┘   └──────┘         └─┘
typ                   └┘   └──────┘           └┘   └──────┘        └─┘
doc                    └┘    └──────┘              └┘    └──────┘
700  by { rw eq, exact continuous_pos_part.comp continuous_neg }
id           └┘        └──────────────────────┘ └────────────┘
src       └─┘└┘  └────┘└──────────────────────┘└────────────┘
typ       └─┘└┘  └────┘└──────────────────────┘└────────────┘
doc       └─┘    └────┘                                      
txt       └─┘    └────┘                                      
par       └─┘    └────┘                                      
pid                                                        
st     └──────┘└──────────────────────────────────────────────┘└┘
701  
702  end pos_part
703  
704  /- TODO: l1 is a complete space -/
705  
706  end l1
707  
708  end measure_theory